take X ; :: thesis: ( X is ComplexNormSpace-like & X is ComplexLinearSpace-like & X is Abelian & X is add-associative & X is right_zeroed & X is right_complementable & X is strict )
thus X is ComplexNormSpace-like by Def11, Lm11; :: thesis: ( X is ComplexLinearSpace-like & X is Abelian & X is add-associative & X is right_zeroed & X is right_complementable & X is strict )
A1: for x, y being VECTOR of X
for x', y' being VECTOR of ((0). V) st x = x' & y = y' holds
( x + y = x' + y' & ( for z being Complex holds z * x = z * x' ) ) ;
thus X is ComplexLinearSpace-like :: thesis: ( X is Abelian & X is add-associative & X is right_zeroed & X is right_complementable & X is strict )

proof

thus for z being Complex
for v, w being VECTOR of X holds z * (v + w) = (z * v) + (z * w) :: according to CLVECT_1:def 2 :: thesis: ( ( for z1, z2 being Complex
for v being VECTOR of X holds (z1 + z2) * v = (z1 * v) + (z2 * v) ) & ( for z1, z2 being Complex
for v being VECTOR of X holds (z1 * z2) * v = z1 * (z2 * v) ) & ( for v being VECTOR of X holds 1r * v = v ) )

proof

let z be Complex; :: thesis: for v, w being VECTOR of X holds z * (v + w) = (z * v) + (z * w)
let v, w be VECTOR of X; :: thesis: z * (v + w) = (z * v) + (z * w)
reconsider v' = v, w' = w as VECTOR of ((0). V) ;
thus z * (v + w) = z * (v' + w')
.= (z * v') + (z * w') by Def2
.= (z * v) + (z * w) ; :: thesis: verum

end;

thus for z1, z2 being Complex
for v being VECTOR of X holds (z1 + z2) * v = (z1 * v) + (z2 * v) :: thesis: ( ( for z1, z2 being Complex
for v being VECTOR of X holds (z1 * z2) * v = z1 * (z2 * v) ) & ( for v being VECTOR of X holds 1r * v = v ) )

proof

let z1, z2 be Complex; :: thesis: for v being VECTOR of X holds (z1 + z2) * v = (z1 * v) + (z2 * v)
let v be VECTOR of X; :: thesis: (z1 + z2) * v = (z1 * v) + (z2 * v)
reconsider v' = v as VECTOR of ((0). V) ;
thus (z1 + z2) * v = (z1 + z2) * v'
.= (z1 * v') + (z2 * v') by Def2
.= (z1 * v) + (z2 * v) ; :: thesis: verum

end;

thus for z1, z2 being Complex
for v being VECTOR of X holds (z1 * z2) * v = z1 * (z2 * v) :: thesis: for v being VECTOR of X holds 1r * v = v

proof

let z1, z2 be Complex; :: thesis: for v being VECTOR of X holds (z1 * z2) * v = z1 * (z2 * v)
let v be VECTOR of X; :: thesis: (z1 * z2) * v = z1 * (z2 * v)
reconsider v' = v as VECTOR of ((0). V) ;
thus (z1 * z2) * v = (z1 * z2) * v'
.= z1 * (z2 * v') by Def2
.= z1 * (z2 * v) ; :: thesis: verum

end;

let v be VECTOR of X; :: thesis: 1r * v = v
reconsider v' = v as VECTOR of ((0). V) ;
thus 1r * v = 1r * v'
.= v by Def2 ; :: thesis: verum

end;

thus for v, w being VECTOR of X holds v + w = w + v :: according to RLVECT_1:def 5 :: thesis: ( X is add-associative & X is right_zeroed & X is right_complementable & X is strict )

proof

let v, w be VECTOR of X; :: thesis: v + w = w + v
reconsider v' = v, w' = w as VECTOR of ((0). V) ;
thus v + w = w' + v' by A1
.= w + v ; :: thesis: verum

end;

thus for u, v, w being VECTOR of X holds (u + v) + w = u + (v + w) :: according to RLVECT_1:def 6 :: thesis: ( X is right_zeroed & X is right_complementable & X is strict )

proof

let u, v, w be VECTOR of X; :: thesis: (u + v) + w = u + (v + w)
reconsider u' = u, v' = v, w' = w as VECTOR of ((0). V) ;
thus (u + v) + w = (u' + v') + w'
.= u' + (v' + w') by RLVECT_1:def 6
.= u + (v + w) ; :: thesis: verum

end;

thus for v being VECTOR of X holds v + (0. X) = v :: according to RLVECT_1:def 7 :: thesis: ( X is right_complementable & X is strict )

proof

let v be VECTOR of X; :: thesis: v + (0. X) = v
reconsider v' = v as VECTOR of ((0). V) ;
thus v + (0. X) = v' + (0. ((0). V))
.= v by RLVECT_1:10 ; :: thesis: verum

end;

thus X is right_complementable :: thesis: X is strict

proof

let v be VECTOR of X; :: according to ALGSTR_0:def 16 :: thesis: v is right_complementable
reconsider v' = v as VECTOR of ((0). V) ;
consider w' being VECTOR of ((0). V) such that
A2: v' + w' = 0. ((0). V) by ALGSTR_0:def 11;
reconsider w = w' as VECTOR of X ;
take w ; :: according to ALGSTR_0:def 11 :: thesis: v + w = 0. X
thus v + w = 0. X by A2; :: thesis: verum

end;

thus X is strict ; :: thesis: verum