let X, Y be RealLinearSpace; :: thesis: for X1, Y1 being Subspace of [:X,Y:] st X1 = [:X,((0). Y):] & Y1 = [:((0). X),Y:] holds
( X1 + Y1 = [:X,Y:] & X1 /\ Y1 = (0). [:X,Y:] )
let X1, Y1 be Subspace of [:X,Y:]; :: thesis: ( X1 = [:X,((0). Y):] & Y1 = [:((0). X),Y:] implies ( X1 + Y1 = [:X,Y:] & X1 /\ Y1 = (0). [:X,Y:] ) )
assume A1: ( X1 = [:X,((0). Y):] & Y1 = [:((0). X),Y:] ) ; :: thesis: ( X1 + Y1 = [:X,Y:] & X1 /\ Y1 = (0). [:X,Y:] )
for x being object holds
( x in the carrier of (X1 + Y1) iff x in the carrier of [:X,Y:] )

proof

let x be object ; :: thesis: ( x in the carrier of (X1 + Y1) iff x in the carrier of [:X,Y:] )

hereby :: thesis: ( x in the carrier of [:X,Y:] implies x in the carrier of (X1 + Y1) )

assume x in the carrier of (X1 + Y1) ; :: thesis: x in the carrier of [:X,Y:]
then x in { (v + u) where u, v is VECTOR of [:X,Y:] : ( v in X1 & u in Y1 ) } by RLSUB_2:def 1;
then consider u, v being VECTOR of [:X,Y:] such that
A2: ( x = v + u & v in X1 & u in Y1 ) ;
thus x in the carrier of [:X,Y:] by A2; :: thesis: verum

end;

assume x in the carrier of [:X,Y:] ; :: thesis: x in the carrier of (X1 + Y1)
then consider a being Point of X, b being Point of Y such that
A3: x = [a,b] by PRVECT_3:9;
reconsider x1 = [a,(0. Y)] as Point of [:X,Y:] ;
reconsider y1 = [(0. X),b] as Point of [:X,Y:] ;
A4: x1 + y1 = [(a + (0. X)),((0. Y) + b)] by PRVECT_3:9
.= [a,b] ;
0. X in {(0. X)} by TARSKI:def 1;
then 0. X in the carrier of ((0). X) by RLSUB_1:def 3;
then [(0. X),b] is Point of [:((0). X),Y:] by PRVECT_3:9;
then A5: y1 in Y1 by A1;
0. Y in {(0. Y)} by TARSKI:def 1;
then 0. Y in the carrier of ((0). Y) by RLSUB_1:def 3;
then [a,(0. Y)] is Point of [:X,((0). Y):] by PRVECT_3:9;
then A6: x1 in X1 by A1;
x in { (v + u) where u, v is VECTOR of [:X,Y:] : ( v in X1 & u in Y1 ) } by A3, A4, A5, A6;
hence x in the carrier of (X1 + Y1) by RLSUB_2:def 1; :: thesis: verum

end;

hence X1 + Y1 = [:X,Y:] by RLSUB_1:32, TARSKI:2; :: thesis: X1 /\ Y1 = (0). [:X,Y:]
A7: for x being object holds
( x in the carrier of [:X,((0). Y):] /\ the carrier of [:((0). X),Y:] iff x in {[(0. X),(0. Y)]} )

proof

let x be object ; :: thesis: ( x in the carrier of [:X,((0). Y):] /\ the carrier of [:((0). X),Y:] iff x in {[(0. X),(0. Y)]} )

hereby :: thesis: ( x in {[(0. X),(0. Y)]} implies x in the carrier of [:X,((0). Y):] /\ the carrier of [:((0). X),Y:] )

assume x in the carrier of [:X,((0). Y):] /\ the carrier of [:((0). X),Y:] ; :: thesis: x in {[(0. X),(0. Y)]}
then A8: ( x in the carrier of [:X,((0). Y):] & x in the carrier of [:((0). X),Y:] ) by XBOOLE_0:def 4;
consider a being Point of X, b being Point of ((0). Y) such that
A9: x = [a,b] by A8, PRVECT_3:9;
consider a1 being Point of ((0). X), b1 being Point of Y such that
A10: x = [a1,b1] by A8, PRVECT_3:9;
A11: ( a = a1 & b = b1 ) by A9, A10, XTUPLE_0:1;
a1 in the carrier of ((0). X) ;
then a1 in {(0. X)} by RLSUB_1:def 3;
then A12: a1 = 0. X by TARSKI:def 1;
b in the carrier of ((0). Y) ;
then A13: b in {(0. Y)} by RLSUB_1:def 3;
x = [(0. X),(0. Y)] by A10, A11, A12, A13, TARSKI:def 1;
hence x in {[(0. X),(0. Y)]} by TARSKI:def 1; :: thesis: verum

end;

assume x in {[(0. X),(0. Y)]} ; :: thesis: x in the carrier of [:X,((0). Y):] /\ the carrier of [:((0). X),Y:]
then A14: x = [(0. X),(0. Y)] by TARSKI:def 1;
0. X in {(0. X)} by TARSKI:def 1;
then A15: 0. X in the carrier of ((0). X) by RLSUB_1:def 3;
0. Y in {(0. Y)} by TARSKI:def 1;
then 0. Y in the carrier of ((0). Y) by RLSUB_1:def 3;
then A16: x is Point of [:X,((0). Y):] by A14, PRVECT_3:9;
x is Point of [:((0). X),Y:] by A14, A15, PRVECT_3:9;
hence x in the carrier of [:X,((0). Y):] /\ the carrier of [:((0). X),Y:] by A16, XBOOLE_0:def 4; :: thesis: verum

end;

the carrier of (X1 /\ Y1) = the carrier of X1 /\ the carrier of Y1 by RLSUB_2:def 2
.= the carrier of [:X,((0). Y):] /\ the carrier of [:((0). X),Y:] by A1
.= {[(0. X),(0. Y)]} by A7, TARSKI:2
.= {(0. [:X,Y:])}
.= the carrier of ((0). [:X,Y:]) by RLSUB_1:def 3 ;
hence X1 /\ Y1 = (0). [:X,Y:] by RLSUB_1:30; :: thesis: verum