let E be RealLinearSpace; :: thesis: for v being Element of E

for A, B being non empty binary-image of E holds

( (v + A) (+) B = A (+) (v + B) & (v + A) (+) B = v + (A (+) B) )

let v be Element of E; :: thesis: for A, B being non empty binary-image of E holds

( (v + A) (+) B = A (+) (v + B) & (v + A) (+) B = v + (A (+) B) )

let A, B be non empty binary-image of E; :: thesis: ( (v + A) (+) B = A (+) (v + B) & (v + A) (+) B = v + (A (+) B) )

for x being object holds

( x in (v + A) (+) B iff x in A (+) (v + B) )

for x being object holds

( x in (v + A) (+) B iff x in v + (A (+) B) )

for A, B being non empty binary-image of E holds

( (v + A) (+) B = A (+) (v + B) & (v + A) (+) B = v + (A (+) B) )

let v be Element of E; :: thesis: for A, B being non empty binary-image of E holds

( (v + A) (+) B = A (+) (v + B) & (v + A) (+) B = v + (A (+) B) )

let A, B be non empty binary-image of E; :: thesis: ( (v + A) (+) B = A (+) (v + B) & (v + A) (+) B = v + (A (+) B) )

for x being object holds

( x in (v + A) (+) B iff x in A (+) (v + B) )

proof

hence
(v + A) (+) B = A (+) (v + B)
by TARSKI:2; :: thesis: (v + A) (+) B = v + (A (+) B)
let x be object ; :: thesis: ( x in (v + A) (+) B iff x in A (+) (v + B) )

then consider a, f being Element of E such that

A4: ( x = a + f & a in A & f in v + B ) ;

consider b being Element of E such that

A5: ( f = v + b & b in B ) by A4;

A6: x = (v + a) + b by A4, A5, RLVECT_1:def 3;

v + a in v + A by A4;

hence x in (v + A) (+) B by A6, A5; :: thesis: verum

end;hereby :: thesis: ( x in A (+) (v + B) implies x in (v + A) (+) B )

assume
x in A (+) (v + B)
; :: thesis: x in (v + A) (+) Bassume
x in (v + A) (+) B
; :: thesis: x in A (+) (v + B)

then consider f, b being Element of E such that

A1: ( x = f + b & f in v + A & b in B ) ;

consider a being Element of E such that

A2: ( f = v + a & a in A ) by A1;

A3: x = a + (v + b) by A1, A2, RLVECT_1:def 3;

v + b in v + B by A1;

hence x in A (+) (v + B) by A3, A2; :: thesis: verum

end;then consider f, b being Element of E such that

A1: ( x = f + b & f in v + A & b in B ) ;

consider a being Element of E such that

A2: ( f = v + a & a in A ) by A1;

A3: x = a + (v + b) by A1, A2, RLVECT_1:def 3;

v + b in v + B by A1;

hence x in A (+) (v + B) by A3, A2; :: thesis: verum

then consider a, f being Element of E such that

A4: ( x = a + f & a in A & f in v + B ) ;

consider b being Element of E such that

A5: ( f = v + b & b in B ) by A4;

A6: x = (v + a) + b by A4, A5, RLVECT_1:def 3;

v + a in v + A by A4;

hence x in (v + A) (+) B by A6, A5; :: thesis: verum

for x being object holds

( x in (v + A) (+) B iff x in v + (A (+) B) )

proof

hence
(v + A) (+) B = v + (A (+) B)
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in (v + A) (+) B iff x in v + (A (+) B) )

then consider ab being Element of E such that

A10: ( x = v + ab & ab in A (+) B ) ;

consider a, b being Element of E such that

A11: ( ab = a + b & a in A & b in B ) by A10;

A12: x = (v + a) + b by A10, A11, RLVECT_1:def 3;

v + a in v + A by A11;

hence x in (v + A) (+) B by A12, A11; :: thesis: verum

end;hereby :: thesis: ( x in v + (A (+) B) implies x in (v + A) (+) B )

assume
x in v + (A (+) B)
; :: thesis: x in (v + A) (+) Bassume
x in (v + A) (+) B
; :: thesis: x in v + (A (+) B)

then consider f, b being Element of E such that

A7: ( x = f + b & f in v + A & b in B ) ;

consider a being Element of E such that

A8: ( f = v + a & a in A ) by A7;

A9: x = v + (a + b) by A7, A8, RLVECT_1:def 3;

a + b in A + B by A7, A8;

hence x in v + (A (+) B) by A9; :: thesis: verum

end;then consider f, b being Element of E such that

A7: ( x = f + b & f in v + A & b in B ) ;

consider a being Element of E such that

A8: ( f = v + a & a in A ) by A7;

A9: x = v + (a + b) by A7, A8, RLVECT_1:def 3;

a + b in A + B by A7, A8;

hence x in v + (A (+) B) by A9; :: thesis: verum

then consider ab being Element of E such that

A10: ( x = v + ab & ab in A (+) B ) ;

consider a, b being Element of E such that

A11: ( ab = a + b & a in A & b in B ) by A10;

A12: x = (v + a) + b by A10, A11, RLVECT_1:def 3;

v + a in v + A by A11;

hence x in (v + A) (+) B by A12, A11; :: thesis: verum