let E be RealLinearSpace; :: thesis: for A, B being non empty binary-image of E holds A (+) B = { v where v is Element of E : (v + ((- 1) * B)) /\ A <> {} }
let A, B be non empty binary-image of E; :: thesis: A (+) B = { v where v is Element of E : (v + ((- 1) * B)) /\ A <> {} }
thus A (+) B c= { v where v is Element of E : (v + ((- 1) * B)) /\ A <> {} } :: according to XBOOLE_0:def 10 :: thesis: { v where v is Element of E : (v + ((- 1) * B)) /\ A <> {} } c= A (+) B
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A (+) B or x in { v where v is Element of E : (v + ((- 1) * B)) /\ A <> {} } )
assume A1: x in A (+) B ; :: thesis: x in { v where v is Element of E : (v + ((- 1) * B)) /\ A <> {} }
consider a0, b0 being Element of E such that
A2: ( x = a0 + b0 & a0 in A & b0 in B ) by A1;
reconsider v = x as Element of E by A1;
A3: v - b0 = a0 by A2, RLVECT_4:1;
(- 1) * b0 in (- 1) * B by A2;
then v + ((- 1) * b0) in v + ((- 1) * B) ;
then v - b0 in v + ((- 1) * B) by RLVECT_1:16;
then (v + ((- 1) * B)) /\ A <> {} by A2, A3, XBOOLE_0:def 4;
hence x in { w where w is Element of E : (w + ((- 1) * B)) /\ A <> {} } ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { v where v is Element of E : (v + ((- 1) * B)) /\ A <> {} } or x in A (+) B )
assume x in { v where v is Element of E : (v + ((- 1) * B)) /\ A <> {} } ; :: thesis: x in A (+) B
then consider v being Element of E such that
A4: ( x = v & (v + ((- 1) * B)) /\ A <> {} ) ;
consider y being object such that
A5: y in (v + ((- 1) * B)) /\ A by A4, XBOOLE_0:def 1;
A6: ( y in v + ((- 1) * B) & y in A ) by A5, XBOOLE_0:def 4;
then consider nb being Element of E such that
A7: ( y = v + nb & nb in (- 1) * B ) ;
consider b being Element of E such that
A8: ( nb = (- 1) * b & b in B ) by A7;
reconsider a = y as Element of E by A7;
a + b = (v - b) + b by A7, A8, RLVECT_1:16
.= v by RLVECT_4:1 ;
hence x in A (+) B by A4, A8, A6; :: thesis: verum