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 5

.= { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) } by RLSUB_2:def 1 ;

for x being object st x in (Up W1) + (Up W2) holds

x in Up (W1 + W2)

for x being object st x in Up (W1 + W2) holds

x in (Up W1) + (Up W2)

hence Up (W1 + W2) = (Up W1) + (Up W2) by A6, XBOOLE_0:def 10; :: thesis: verum

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 5

.= { (v + u) where u, v is VECTOR of V : ( v in W1 & u in W2 ) } by RLSUB_2:def 1 ;

for x being object st x in (Up W1) + (Up W2) holds

x in Up (W1 + W2)

proof

then A6:
(Up W1) + (Up W2) c= Up (W1 + W2)
;
let x be object ; :: 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 9;

then consider u, v being Element of V such that

A2: x = u + v and

A3: u in Up W1 and

A4: v in Up W2 ;

v in the carrier of W2 by A4, RUSUB_4:def 5;

then A5: v in W2 by STRUCT_0:def 5;

u in the carrier of W1 by A3, RUSUB_4:def 5;

then u in W1 by STRUCT_0:def 5;

hence x in Up (W1 + W2) by A1, A2, A5; :: thesis: verum

end;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 9;

then consider u, v being Element of V such that

A2: x = u + v and

A3: u in Up W1 and

A4: v in Up W2 ;

v in the carrier of W2 by A4, RUSUB_4:def 5;

then A5: v in W2 by STRUCT_0:def 5;

u in the carrier of W1 by A3, RUSUB_4:def 5;

then u in W1 by STRUCT_0:def 5;

hence x in Up (W1 + W2) by A1, A2, A5; :: thesis: verum

for x being object st x in Up (W1 + W2) holds

x in (Up W1) + (Up W2)

proof

then
Up (W1 + W2) c= (Up W1) + (Up W2)
;
let x be object ; :: 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 u, v being VECTOR of V such that

A7: x = v + u and

A8: v in W1 and

A9: u in W2 by A1;

u in the carrier of W2 by A9, STRUCT_0:def 5;

then A10: u in Up W2 by RUSUB_4:def 5;

v in the carrier of W1 by A8, STRUCT_0:def 5;

then v in Up W1 by RUSUB_4:def 5;

then x in { (u9 + v9) where u9, v9 is Element of V : ( u9 in Up W1 & v9 in Up W2 ) } by A7, A10;

hence x in (Up W1) + (Up W2) by RUSUB_4:def 9; :: thesis: verum

end;assume x in Up (W1 + W2) ; :: thesis: x in (Up W1) + (Up W2)

then consider u, v being VECTOR of V such that

A7: x = v + u and

A8: v in W1 and

A9: u in W2 by A1;

u in the carrier of W2 by A9, STRUCT_0:def 5;

then A10: u in Up W2 by RUSUB_4:def 5;

v in the carrier of W1 by A8, STRUCT_0:def 5;

then v in Up W1 by RUSUB_4:def 5;

then x in { (u9 + v9) where u9, v9 is Element of V : ( u9 in Up W1 & v9 in Up W2 ) } by A7, A10;

hence x in (Up W1) + (Up W2) by RUSUB_4:def 9; :: thesis: verum

hence Up (W1 + W2) = (Up W1) + (Up W2) by A6, XBOOLE_0:def 10; :: thesis: verum