let X be RealLinearSpace; :: thesis: for Y1, Y2 being Subspace of X st Y1 /\ Y2 = (0). X holds
for B1 being Basis of Y1
for B2 being Basis of Y2 holds B1 \/ B2 is Basis of Y1 + Y2
let Y1, Y2 be Subspace of X; :: thesis: ( Y1 /\ Y2 = (0). X implies for B1 being Basis of Y1
for B2 being Basis of Y2 holds B1 \/ B2 is Basis of Y1 + Y2 )
assume A1: Y1 /\ Y2 = (0). X ; :: thesis: for B1 being Basis of Y1
for B2 being Basis of Y2 holds B1 \/ B2 is Basis of Y1 + Y2
let B1 be Basis of Y1; :: thesis: for B2 being Basis of Y2 holds B1 \/ B2 is Basis of Y1 + Y2
let B2 be Basis of Y2; :: thesis: B1 \/ B2 is Basis of Y1 + Y2
A2: (RLSp2RVSp Y1) /\ (RLSp2RVSp Y2) = RLSp2RVSp (Y1 /\ Y2) by Th17
.= (0). (RLSp2RVSp X) by A1, Th18 ;
A3: B1 is Basis of (RLSp2RVSp Y1) by REAL_NS2:80;
A4: B2 is Basis of (RLSp2RVSp Y2) by REAL_NS2:80;
RLSp2RVSp (Y1 + Y2) = (RLSp2RVSp Y1) + (RLSp2RVSp Y2) by Th16;
then B1 \/ B2 is Basis of (RLSp2RVSp (Y1 + Y2)) by A2, A3, A4, MATRLIN2:3;
hence B1 \/ B2 is Basis of Y1 + Y2 by REAL_NS2:80; :: thesis: verum