take CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) ; :: thesis: ( CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is ComplexUnitarySpace-like & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is vector-distributive & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is scalar-distributive & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is scalar-associative & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is scalar-unital & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is Abelian & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is add-associative & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is right_zeroed & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is right_complementable & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is strict )
thus CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is ComplexUnitarySpace-like by Lm9; :: thesis: ( CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is vector-distributive & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is scalar-distributive & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is scalar-associative & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is scalar-unital & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is Abelian & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is add-associative & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is right_zeroed & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is right_complementable & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is strict )
thus ( CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is vector-distributive & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is scalar-distributive & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is scalar-associative & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is scalar-unital ) :: thesis: ( CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is Abelian & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is add-associative & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is right_zeroed & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is right_complementable & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is strict )

proof

thus for a being Complex
for v, w being VECTOR of CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) holds a * (v + w) = (a * v) + (a * w) :: according to CLVECT_1:def 2 :: thesis: ( CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is scalar-distributive & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is scalar-associative & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is scalar-unital )

proof

let a be Complex; :: thesis: for v, w being VECTOR of CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) holds a * (v + w) = (a * v) + (a * w)
let v, w be VECTOR of CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #); :: thesis: a * (v + w) = (a * v) + (a * w)
reconsider v9 = v, w9 = w as VECTOR of ((0). the ComplexLinearSpace) ;
thus a * (v + w) = a * (v9 + w9)
.= (a * v9) + (a * w9) by CLVECT_1:def 2
.= (a * v) + (a * w) ; :: thesis: verum

end;

thus for a, b being Complex
for v being VECTOR of CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) holds (a + b) * v = (a * v) + (b * v) :: according to CLVECT_1:def 3 :: thesis: ( CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is scalar-associative & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is scalar-unital )

proof

let a, b be Complex; :: thesis: for v being VECTOR of CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) holds (a + b) * v = (a * v) + (b * v)
let v be VECTOR of CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #); :: thesis: (a + b) * v = (a * v) + (b * v)
reconsider v9 = v as VECTOR of ((0). the ComplexLinearSpace) ;
thus (a + b) * v = (a + b) * v9
.= (a * v9) + (b * v9) by CLVECT_1:def 3
.= (a * v) + (b * v) ; :: thesis: verum

end;

thus for a, b being Complex
for v being VECTOR of CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) holds (a * b) * v = a * (b * v) :: according to CLVECT_1:def 4 :: thesis: CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is scalar-unital

proof

let a, b be Complex; :: thesis: for v being VECTOR of CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) holds (a * b) * v = a * (b * v)
let v be VECTOR of CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #); :: thesis: (a * b) * v = a * (b * v)
reconsider v9 = v as VECTOR of ((0). the ComplexLinearSpace) ;
thus (a * b) * v = (a * b) * v9
.= a * (b * v9) by CLVECT_1:def 4
.= a * (b * v) ; :: thesis: verum

end;

let v be VECTOR of CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #); :: according to CLVECT_1:def 5 :: thesis: 1r * v = v
reconsider v9 = v as VECTOR of ((0). the ComplexLinearSpace) ;
thus 1r * v = 1r * v9
.= v by CLVECT_1:def 5 ; :: thesis: verum

end;

A1: for x, y being VECTOR of CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #)
for x9, y9 being VECTOR of ((0). the ComplexLinearSpace) st x = x9 & y = y9 holds
( x + y = x9 + y9 & ( for a being Complex holds a * x = a * x9 ) ) ;
thus for v, w being VECTOR of CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) holds v + w = w + v :: according to RLVECT_1:def 2 :: thesis: ( CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is add-associative & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is right_zeroed & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is right_complementable & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is strict )

proof

let v, w be VECTOR of CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #); :: thesis: v + w = w + v
reconsider v9 = v, w9 = w as VECTOR of ((0). the ComplexLinearSpace) ;
thus v + w = w9 + v9 by A1
.= w + v ; :: thesis: verum

end;

thus for u, v, w being VECTOR of CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) holds (u + v) + w = u + (v + w) :: according to RLVECT_1:def 3 :: thesis: ( CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is right_zeroed & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is right_complementable & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is strict )

proof

let u, v, w be VECTOR of CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #); :: thesis: (u + v) + w = u + (v + w)
reconsider u9 = u, v9 = v, w9 = w as VECTOR of ((0). the ComplexLinearSpace) ;
thus (u + v) + w = (u9 + v9) + w9
.= u9 + (v9 + w9) by RLVECT_1:def 3
.= u + (v + w) ; :: thesis: verum

end;

thus for v being VECTOR of CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) holds v + (0. CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #)) = v :: according to RLVECT_1:def 4 :: thesis: ( CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is right_complementable & CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is strict )

proof

let v be VECTOR of CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #); :: thesis: v + (0. CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #)) = v
reconsider v9 = v as VECTOR of ((0). the ComplexLinearSpace) ;
thus v + (0. CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #)) = v9 + (0. ((0). the ComplexLinearSpace))
.= v by RLVECT_1:4 ; :: thesis: verum

end;

thus CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is right_complementable :: thesis: CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is strict

proof

let v be VECTOR of CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #); :: according to ALGSTR_0:def 16 :: thesis: v is right_complementable
reconsider v9 = v as VECTOR of ((0). the ComplexLinearSpace) ;
consider w9 being VECTOR of ((0). the ComplexLinearSpace) such that
A2: v9 + w9 = 0. ((0). the ComplexLinearSpace) by ALGSTR_0:def 11;
reconsider w = w9 as VECTOR of CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) ;
take w ; :: according to ALGSTR_0:def 11 :: thesis: v + w = 0. CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #)
thus v + w = 0. CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) by A2; :: thesis: verum

end;

thus CUNITSTR(# the carrier of ((0). the ComplexLinearSpace),(0. ((0). the ComplexLinearSpace)), the addF of ((0). the ComplexLinearSpace), the Mult of ((0). the ComplexLinearSpace),nilfunc #) is strict ; :: thesis: verum