let V be RealLinearSpace; :: thesis: for A, B being Subset of V holds Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B)

let A, B be Subset of V; :: thesis: Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B)

( Lin (A /\ B) is Subspace of Lin A & Lin (A /\ B) is Subspace of Lin B ) by Th20, XBOOLE_1:17;

hence Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B) by Lm4; :: thesis: verum

let A, B be Subset of V; :: thesis: Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B)

( Lin (A /\ B) is Subspace of Lin A & Lin (A /\ B) is Subspace of Lin B ) by Th20, XBOOLE_1:17;

hence Lin (A /\ B) is Subspace of (Lin A) /\ (Lin B) by Lm4; :: thesis: verum