let V be RealUnitarySpace; for W1, W2, W3 being Subspace of V holds W1 + (W2 + W3) = (W1 + W2) + W3
let W1, W2, W3 be Subspace of V; W1 + (W2 + W3) = (W1 + W2) + W3
set A = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } ;
set B = { (v + u) where v, u is VECTOR of V : ( v in W2 & u in W3 ) } ;
set C = { (v + u) where v, u is VECTOR of V : ( v in W1 + W2 & u in W3 ) } ;
set D = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 + W3 ) } ;
A1:
the carrier of (W1 + (W2 + W3)) = { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 + W3 ) }
by Def1;
A2:
{ (v + u) where v, u is VECTOR of V : ( v in W1 + W2 & u in W3 ) } c= { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 + W3 ) }
proof
let x be
object ;
TARSKI:def 3 ( not x in { (v + u) where v, u is VECTOR of V : ( v in W1 + W2 & u in W3 ) } or x in { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 + W3 ) } )
assume
x in { (v + u) where v, u is VECTOR of V : ( v in W1 + W2 & u in W3 ) }
;
x in { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 + W3 ) }
then consider v,
u being
VECTOR of
V such that A3:
x = v + u
and A4:
v in W1 + W2
and A5:
u in W3
;
v in the
carrier of
(W1 + W2)
by A4, STRUCT_0:def 5;
then
v in { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) }
by Def1;
then consider u1,
u2 being
VECTOR of
V such that A6:
v = u1 + u2
and A7:
u1 in W1
and A8:
u2 in W2
;
u2 + u in { (v + u) where v, u is VECTOR of V : ( v in W2 & u in W3 ) }
by A5, A8;
then
u2 + u in the
carrier of
(W2 + W3)
by Def1;
then A9:
u2 + u in W2 + W3
by STRUCT_0:def 5;
v + u = u1 + (u2 + u)
by A6, RLVECT_1:def 3;
hence
x in { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 + W3 ) }
by A3, A7, A9;
verum
end;
{ (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 + W3 ) } c= { (v + u) where v, u is VECTOR of V : ( v in W1 + W2 & u in W3 ) }
proof
let x be
object ;
TARSKI:def 3 ( not x in { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 + W3 ) } or x in { (v + u) where v, u is VECTOR of V : ( v in W1 + W2 & u in W3 ) } )
assume
x in { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 + W3 ) }
;
x in { (v + u) where v, u is VECTOR of V : ( v in W1 + W2 & u in W3 ) }
then consider v,
u being
VECTOR of
V such that A10:
x = v + u
and A11:
v in W1
and A12:
u in W2 + W3
;
u in the
carrier of
(W2 + W3)
by A12, STRUCT_0:def 5;
then
u in { (v + u) where v, u is VECTOR of V : ( v in W2 & u in W3 ) }
by Def1;
then consider u1,
u2 being
VECTOR of
V such that A13:
u = u1 + u2
and A14:
u1 in W2
and A15:
u2 in W3
;
v + u1 in { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) }
by A11, A14;
then
v + u1 in the
carrier of
(W1 + W2)
by Def1;
then A16:
v + u1 in W1 + W2
by STRUCT_0:def 5;
v + u = (v + u1) + u2
by A13, RLVECT_1:def 3;
hence
x in { (v + u) where v, u is VECTOR of V : ( v in W1 + W2 & u in W3 ) }
by A10, A15, A16;
verum
end;
then
{ (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 + W3 ) } = { (v + u) where v, u is VECTOR of V : ( v in W1 + W2 & u in W3 ) }
by A2;
hence
W1 + (W2 + W3) = (W1 + W2) + W3
by A1, Def1; verum