let V be RealLinearSpace; :: thesis: for W1, W2 being Subspace of V holds Up (W1 + W2) = (Up W1) + (Up W2)
let W1, W2 be Subspace of V; :: thesis: Up (W1 + W2) = (Up W1) + (Up W2)
A1: Up (W1 + W2) = the carrier of (W1 + W2) by RUSUB_4:def 6
.= { (v + u) where v, u is VECTOR of V : ( v in W1 & u in W2 ) } by RLSUB_2:def 1 ;
for x being set st x in Up (W1 + W2) holds
x in (Up W1) + (Up W2)

proof

let x be set ; :: thesis: ( x in Up (W1 + W2) implies x in (Up W1) + (Up W2) )
assume x in Up (W1 + W2) ; :: thesis: x in (Up W1) + (Up W2)
then consider v, u being VECTOR of V such that
A2: ( x = v + u & v in W1 & u in W2 ) by A1;
( v in the carrier of W1 & u in the carrier of W2 ) by A2, STRUCT_0:def 5;
then ( v in Up W1 & u in Up W2 ) by RUSUB_4:def 6;
then x in { (u' + v') where u', v' is Element of V : ( u' in Up W1 & v' in Up W2 ) } by A2;
hence x in (Up W1) + (Up W2) by RUSUB_4:def 10; :: thesis: verum

end;

then A3: Up (W1 + W2) c= (Up W1) + (Up W2) by TARSKI:def 3;
for x being set st x in (Up W1) + (Up W2) holds
x in Up (W1 + W2)

proof

let x be set ; :: thesis: ( x in (Up W1) + (Up W2) implies x in Up (W1 + W2) )
assume x in (Up W1) + (Up W2) ; :: thesis: x in Up (W1 + W2)
then x in { (u + v) where u, v is Element of V : ( u in Up W1 & v in Up W2 ) } by RUSUB_4:def 10;
then consider u, v being Element of V such that
A4: ( x = u + v & u in Up W1 & v in Up W2 ) ;
( u in the carrier of W1 & v in the carrier of W2 ) by A4, RUSUB_4:def 6;
then ( u in W1 & v in W2 ) by STRUCT_0:def 5;
hence x in Up (W1 + W2) by A1, A4; :: thesis: verum

end;

then (Up W1) + (Up W2) c= Up (W1 + W2) by TARSKI:def 3;
hence Up (W1 + W2) = (Up W1) + (Up W2) by A3, XBOOLE_0:def 10; :: thesis: verum