let X, Y be RealLinearSpace; :: thesis: for BX being Basis of X
for BY being Basis of Y holds [:BX,{(0. Y)}:] \/ [:{(0. X)},BY:] is Basis of [:X,Y:]
let BX be Basis of X; :: thesis: for BY being Basis of Y holds [:BX,{(0. Y)}:] \/ [:{(0. X)},BY:] is Basis of [:X,Y:]
let BY be Basis of Y; :: thesis: [:BX,{(0. Y)}:] \/ [:{(0. X)},BY:] is Basis of [:X,Y:]
reconsider BBX = [:BX,{(0. Y)}:] as Subset of the carrier of [:X,Y:] by ZFMISC_1:96;
reconsider BBY = [:{(0. X)},BY:] as Subset of the carrier of [:X,Y:] by ZFMISC_1:96;
reconsider BB = BBX \/ BBY as Subset of the carrier of [:X,Y:] ;
consider T1 being LinearOperator of X,[:X,((0). Y):] such that
A1: T1 is bijective and
A2: for x being Element of X holds T1 . x = [x,(0. Y)] by Th23;
for y being object holds
( y in T1 .: BX iff y in BBX )

proof

let y be object ; :: thesis: ( y in T1 .: BX iff y in BBX )

hereby :: thesis: ( y in BBX implies y in T1 .: BX )

assume y in T1 .: BX ; :: thesis: y in BBX
then consider x being object such that
A3: ( x in the carrier of X & x in BX & y = T1 . x ) by FUNCT_2:64;
A4: y = [x,(0. Y)] by A2, A3;
0. Y in {(0. Y)} by TARSKI:def 1;
hence y in BBX by A3, A4, ZFMISC_1:87; :: thesis: verum

end;

assume y in BBX ; :: thesis: y in T1 .: BX
then consider a, b being object such that
A5: ( a in BX & b in {(0. Y)} & y = [a,b] ) by ZFMISC_1:def 2;
A6: b = 0. Y by A5, TARSKI:def 1;
T1 . a = [a,(0. Y)] by A2, A5;
hence y in T1 .: BX by A5, A6, FUNCT_2:35; :: thesis: verum

end;

then A7: T1 .: BX = BBX by TARSKI:2;
consider T2 being LinearOperator of Y,[:((0). X),Y:] such that
A8: T2 is bijective and
A9: for y being Element of Y holds T2 . y = [(0. X),y] by Th24;
for y being object holds
( y in T2 .: BY iff y in BBY )

proof

let y be object ; :: thesis: ( y in T2 .: BY iff y in BBY )

hereby :: thesis: ( y in BBY implies y in T2 .: BY )

assume y in T2 .: BY ; :: thesis: y in BBY
then consider x being object such that
A10: ( x in the carrier of Y & x in BY & y = T2 . x ) by FUNCT_2:64;
A11: y = [(0. X),x] by A9, A10;
0. X in {(0. X)} by TARSKI:def 1;
hence y in BBY by A10, A11, ZFMISC_1:87; :: thesis: verum

end;

assume y in BBY ; :: thesis: y in T2 .: BY
then consider a, b being object such that
A12: ( a in {(0. X)} & b in BY & y = [a,b] ) by ZFMISC_1:def 2;
A13: a = 0. X by A12, TARSKI:def 1;
T2 . b = [(0. X),b] by A9, A12;
hence y in T2 .: BY by A12, A13, FUNCT_2:35; :: thesis: verum

end;

then A14: T2 .: BY = BBY by TARSKI:2;
X is Subspace of X by RLSUB_1:25;
then reconsider W1 = [:X,((0). Y):] as Subspace of [:X,Y:] by Th21;
Y is Subspace of Y by RLSUB_1:25;
then reconsider W2 = [:((0). X),Y:] as Subspace of [:X,Y:] by Th21;
A15: BBX is Basis of W1 by A1, A7, REAL_NS2:87;
A16: BBY is Basis of W2 by A8, A14, REAL_NS2:87;
( W1 + W2 = [:X,Y:] & W1 /\ W2 = (0). [:X,Y:] ) by Th22;
hence [:BX,{(0. Y)}:] \/ [:{(0. X)},BY:] is Basis of [:X,Y:] by A15, A16, Th20; :: thesis: verum