(=> (= (The-Dyad ?M ?B) ?T)
(= ?T
(Summation (Lambda (?I)
(Summation (Lambda (?J)
(* (Basis.Vec ?B ?I)
(* (Value ?M ?I ?J)
(Basis.Vec ?B ?J))))
1
(Spatial.Dimension ?T)))
1
(Spatial.Dimension ?T))))
(=> (= (The-Dyad ?M ?B) ?T) (Dyad ?T))
(=> (= (The-Dyad ?M ?B) ?T) (= (Spatial.Dimension ?T) (Size ?M)))
(=> (= (The-Dyad ?M ?B) ?T) (= (Size ?M) (Basis.Dimension ?B)))
(=> (= (The-Dyad ?M ?B) ?T)
(= (Quantity.Dimension ?T) (Quantity.Dimension ?M)))
(=> (= (The-Dyad ?M ?B) ?T) (Orthonormal-Basis ?B))
(=> (= (The-Dyad ?M ?B) ?T) (Square-Matrix ?M))
(=> (= (The-Dyad ?M ?B) ?T) (Matrix-Quantity ?M))
(=> (And (Dyad ?T1) (Dyad ?T2))
(<=> (Dot ?T1 ?T2 ?T)
(And (Dyad ?T)
(Forall (?B)
(= ?T
(The-Dyad (* (Tensor-To-Matrix ?T1 ?B)
(Tensor-To-Matrix ?T2 ?B))
?B)))
(Forall
(?B ?I ?J)
(=> (= (Basis.Dimension ?B)
(Spatial.Dimension ?T1))
(= ?T
(Summation
(Lambda
(?I)
(Summation
(Lambda (?J)
(* (* (Basis.Vec ?B ?I)
(Basis.Vec ?B ?J))
(* (Dyad-Component ?T1
?I
?J
?B)
(Dyad-Component ?T2
?J
?I
?B))))
1
(Spatial.Dimension ?T1)))
1
(Spatial.Dimension ?T1))))))))