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