:: MORPH_01 semantic presentation

begin

definition
let E be non empty RLSStruct ;
mode binary-image of E is Subset of E;
end;


definition
let E be RealLinearSpace;
let A, B be binary-image of E;
funcA (-) B ->  binary-image of E equals :: MORPH_01:def 1
 {  z where z is Element of E : for b being Element of E st b in B holds
z - b in A  }  ;
correctness
coherence
{  z where z is Element of E : for b being Element of E st b in B holds
z - b in A  }  is binary-image of E;
proof
now__::_thesis:_for_x_being_set_st_x_in__{__z_where_z_is_Element_of_E_:_for_b_being_Element_of_E_st_b_in_B_holds_
z_-_b_in_A__}__holds_
x_in_the_carrier_of_E
let x be set ; ::_thesis: ( x in  {  z where z is Element of E : for b being Element of E st b in B holds
z - b in A  }  implies x in the carrier of E )
assume  x in  {  z where z is Element of E : for b being Element of E st b in B holds
z - b in A  }  ; ::_thesis: x in the carrier of E
then  ex z being Element of E st
( x = z & ( for b being Element of E st b in B holds
z - b in A ) ) ;
hence  x in the carrier of E ; ::_thesis: verum
end;
hence   {  z where z is Element of E : for b being Element of E st b in B holds
z - b in A  }  is binary-image of E by TARSKI:def_3; ::_thesis: verum
end;
end;

:: deftheorem  defines (-) MORPH_01:def_1_:_
 for E being RealLinearSpace
for A, B being binary-image of E holds A (-) B =  {  z where z is Element of E : for b being Element of E st b in B holds
z - b in A  }  ;

notation
let a be Real;
let E be RealLinearSpace;
let A be Subset of E;
synonym a * A for a (.) A;
end;

theorem LM0010: :: MORPH_01:1
for E being RealLinearSpace
for A, B being Subset of E st B = {} holds
( A (+) B = B & B (+) A = B & A (-) B = the carrier of E )
proof
let E be RealLinearSpace; ::_thesis: for A, B being Subset of E st B = {} holds
( A (+) B = B & B (+) A = B & A (-) B = the carrier of E )
let A, B be Subset of E; ::_thesis: ( B = {} implies ( A (+) B = B & B (+) A = B & A (-) B = the carrier of E ) )
assume AS: B = {} ; ::_thesis: ( A (+) B = B & B (+) A = B & A (-) B = the carrier of E )
hence  ( A (+) B = B & B (+) A = B ) by RUSUB_5:5; ::_thesis: A (-) B = the carrier of E
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_E_holds_
x_in_A_(-)_B
let x be set ; ::_thesis: ( x in the carrier of E implies x in A (-) B )
assume  x in the carrier of E ; ::_thesis: x in A (-) B
then reconsider z = x as Element of E ;
 for b being Element of E st b in B holds
z - b in A by AS;
hence  x in A (-) B ; ::_thesis: verum
end;
then  the carrier of E c= A (-) B by TARSKI:def_3;
hence  the carrier of E = A (-) B by XBOOLE_0:def_10; ::_thesis: verum
end;

theorem LM0010A: :: MORPH_01:2
for E being RealLinearSpace
for A, B being Subset of E st A <> {} & B = {} holds
B (-) A = B
proof
let E be RealLinearSpace; ::_thesis: for A, B being Subset of E st A <> {} & B = {} holds
B (-) A = B
let A, B be Subset of E; ::_thesis: ( A <> {} & B = {} implies B (-) A = B )
assume AS: ( A <> {} & B = {} ) ; ::_thesis: B (-) A = B
then consider a being set  such that
P1: a in A by XBOOLE_0:def_1;
reconsider a = a as Element of E by P1;
assume  B (-) A <> B ; ::_thesis: contradiction
then consider ba being set  such that
P2: ba in B (-) A by AS, XBOOLE_0:def_1;
consider z being Element of E such that
P3: ( ba = z & ( for a being Element of E st a in A holds
z - a in B ) ) by P2;
thus  contradiction by AS, P1, P3; ::_thesis: verum
end;

theorem LM0020: :: MORPH_01:3
for E being RealLinearSpace
for A, B being Subset of E st B = the carrier of E & A <> {} holds
( A (+) B = B & B (+) A = B )
proof
let E be RealLinearSpace; ::_thesis: for A, B being Subset of E st B = the carrier of E & A <> {} holds
( A (+) B = B & B (+) A = B )
let A, B be Subset of E; ::_thesis: ( B = the carrier of E & A <> {} implies ( A (+) B = B & B (+) A = B ) )
assume AS: ( B = the carrier of E & A <> {} ) ; ::_thesis: ( A (+) B = B & B (+) A = B )
then consider a being set  such that
P1: a in A by XBOOLE_0:def_1;
reconsider a = a as Element of E by P1;
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_E_holds_
x_in_A_(+)_B
let x be set ; ::_thesis: ( x in the carrier of E implies x in A (+) B )
assume  x in the carrier of E ; ::_thesis: x in A (+) B
then reconsider z = x as Element of E ;
 a + (z - a) = z by RLVECT_4:1;
hence  x in A (+) B by AS, P1; ::_thesis: verum
end;
then P1: the carrier of E c= A (+) B by TARSKI:def_3;
hence  B = A (+) B by AS, XBOOLE_0:def_10; ::_thesis: B (+) A = B
thus B (+) A = A + B
.= B by P1, AS, XBOOLE_0:def_10 ; ::_thesis: verum
end;

theorem LM0020A: :: MORPH_01:4
for E being RealLinearSpace
for A, B being Subset of E st B = the carrier of E holds
B (-) A = B
proof
let E be RealLinearSpace; ::_thesis: for A, B being Subset of E st B = the carrier of E holds
B (-) A = B
let A, B be Subset of E; ::_thesis: ( B = the carrier of E implies B (-) A = B )
assume AS: B = the carrier of E ; ::_thesis: B (-) A = B
now__::_thesis:_for_x_being_set_st_x_in_the_carrier_of_E_holds_
x_in_B_(-)_A
let x be set ; ::_thesis: ( x in the carrier of E implies x in B (-) A )
assume  x in the carrier of E ; ::_thesis: x in B (-) A
then reconsider z = x as Element of E ;
 for a being Element of E st a in A holds
z - a in B by AS;
hence  x in B (-) A ; ::_thesis: verum
end;
then  the carrier of E c= B (-) A by TARSKI:def_3;
hence  B = B (-) A by XBOOLE_0:def_10, AS; ::_thesis: verum
end;

theorem :: MORPH_01:5
for E being RealLinearSpace
for A, B being binary-image of E holds A (+) B = union  {  (b + A) where b is Element of E : b in B  }
proof
let E be RealLinearSpace; ::_thesis: for A, B being binary-image of E holds A (+) B = union  {  (b + A) where b is Element of E : b in B  }
let A, B be binary-image of E; ::_thesis: A (+) B = union  {  (b + A) where b is Element of E : b in B  }
now__::_thesis:_for_x_being_set_st_x_in_A_(+)_B_holds_
x_in_union__{__(b_+_A)_where_b_is_Element_of_E_:_b_in_B__}_
let x be set ; ::_thesis: ( x in A (+) B implies x in union  {  (b + A) where b is Element of E : b in B  }  )
assume P1: x in A (+) B ; ::_thesis: x in union  {  (b + A) where b is Element of E : b in B  }
consider a0, b0 being Element of E such that
P2: ( x = a0 + b0 & a0 in A & b0 in B ) by P1;
P3: x in b0 + A by P2;
 b0 + A in  {  (b + A) where b is Element of E : b in B  }  by P2;
hence  x in union  {  (b + A) where b is Element of E : b in B  }  by P3, TARSKI:def_4; ::_thesis: verum
end;
hence  A (+) B c= union  {  (b + A) where b is Element of E : b in B  }  by TARSKI:def_3; :: according to XBOOLE_0:def_10 ::_thesis: union  {  (b + A) where b is Element of E : b in B  }  c= A (+) B
now__::_thesis:_for_x_being_set_st_x_in_union__{__(b_+_A)_where_b_is_Element_of_E_:_b_in_B__}__holds_
x_in_A_(+)_B
let x be set ; ::_thesis: ( x in union  {  (b + A) where b is Element of E : b in B  }  implies x in A (+) B )
assume  x in union  {  (b + A) where b is Element of E : b in B  }  ; ::_thesis: x in A (+) B
then consider y being set  such that
P0: ( x in y & y in  {  (b + A) where b is Element of E : b in B  }  ) by TARSKI:def_4;
consider b being Element of E such that
P1: ( y = b + A & b in B ) by P0;
consider a being Element of E such that
P2: ( x = b + a & a in A ) by P1, P0;
thus  x in A (+) B by P1, P2; ::_thesis: verum
end;
hence  union  {  (b + A) where b is Element of E : b in B  }  c= A (+) B by TARSKI:def_3; ::_thesis: verum
end;

definition
let E be non empty RLSStruct ;
mode binary-image-family of E is Subset-Family of the carrier of E;
end;


theorem :: MORPH_01:6
for E being RealLinearSpace
for A, B being non empty binary-image of E holds A (-) B = meet  {  (b + A) where b is Element of E : b in B  }
proof
let E be RealLinearSpace; ::_thesis: for A, B being non empty binary-image of E holds A (-) B = meet  {  (b + A) where b is Element of E : b in B  }
let A, B be non empty binary-image of E; ::_thesis: A (-) B = meet  {  (b + A) where b is Element of E : b in B  }
consider g being set  such that
P01: g in B by XBOOLE_0:def_1;
reconsider g = g as Element of E by P01;
P02: g + A in  {  (b + A) where b is Element of E : b in B  }  by P01;
now__::_thesis:_for_x_being_set_st_x_in_A_(-)_B_holds_
x_in_meet__{__(b_+_A)_where_b_is_Element_of_E_:_b_in_B__}_
let x be set ; ::_thesis: ( x in A (-) B implies x in meet  {  (b + A) where b is Element of E : b in B  }  )
assume  x in A (-) B ; ::_thesis: x in meet  {  (b + A) where b is Element of E : b in B  }
then consider z being Element of E such that
P1: ( x = z & ( for b being Element of E st b in B holds
z - b in A ) ) ;
 for Y being set st Y in  {  (b + A) where b is Element of E : b in B  }  holds
z in Y
proof
let Y be set ; ::_thesis: ( Y in  {  (b + A) where b is Element of E : b in B  }  implies z in Y )
assume  Y in  {  (b + A) where b is Element of E : b in B  }  ; ::_thesis: z in Y
then consider b being Element of E such that
A2: ( Y = b + A & b in B ) ;
A3: z - b in A by P1, A2;
 z = b + (z - b) by RLVECT_4:1;
hence  z in Y by A3, A2; ::_thesis: verum
end;
hence  x in meet  {  (b + A) where b is Element of E : b in B  }  by P1, P02, SETFAM_1:def_1; ::_thesis: verum
end;
hence  A (-) B c= meet  {  (b + A) where b is Element of E : b in B  }  by TARSKI:def_3; :: according to XBOOLE_0:def_10 ::_thesis: meet  {  (b + A) where b is Element of E : b in B  }  c= A (-) B
now__::_thesis:_for_x_being_set_st_x_in_meet__{__(b_+_A)_where_b_is_Element_of_E_:_b_in_B__}__holds_
x_in_A_(-)_B
let x be set ; ::_thesis: ( x in meet  {  (b + A) where b is Element of E : b in B  }  implies x in A (-) B )
assume P0: x in meet  {  (b + A) where b is Element of E : b in B  }  ; ::_thesis: x in A (-) B
consider S being set  such that
P11: S in  {  (b + A) where b is Element of E : b in B  }  by P02;
consider d being Element of E such that
P12: ( S = d + A & d in B ) by P11;
 x in S by P0, P11, SETFAM_1:def_1;
then reconsider x0 = x as Element of E by P12;
 for b being Element of E st b in B holds
x0 - b in A
proof
let b be Element of E; ::_thesis: ( b in B implies x0 - b in A )
assume  b in B ; ::_thesis: x0 - b in A
then  b + A in  {  (f + A) where f is Element of E : f in B  }  ;
then  x in b + A by P0, SETFAM_1:def_1;
then consider a being Element of E such that
X1: ( x0 = b + a & a in A ) ;
thus  x0 - b in A by X1, RLVECT_4:1; ::_thesis: verum
end;
hence  x in A (-) B ; ::_thesis: verum
end;
hence  meet  {  (b + A) where b is Element of E : b in B  }  c= A (-) B by TARSKI:def_3; ::_thesis: verum
end;

theorem Th104: :: MORPH_01:7
for E being RealLinearSpace
for A, B being non empty binary-image of E holds A (+) B =  {  v where v is Element of E : (v + ((- 1) * B)) /\ A <> {}  }
proof
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 set ; :: 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 P1: 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
P2: ( x = a0 + b0 & a0 in A & b0 in B ) by P1;
reconsider v = x as Element of E by P1;
P3: v - b0 = a0 by P2, RLVECT_4:1;
 (- 1) * b0 in (- 1) * B by P2;
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 P2, P3, XBOOLE_0:def_4;
hence  x in  {  w where w is Element of E : (w + ((- 1) * B)) /\ A <> {}  }  ; ::_thesis: verum
end;
let x be set ; :: 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
P1: ( x = v & (v + ((- 1) * B)) /\ A <> {} ) ;
consider y being set  such that
X1: y in (v + ((- 1) * B)) /\ A by P1, XBOOLE_0:def_1;
X2: ( y in v + ((- 1) * B) & y in A ) by X1, XBOOLE_0:def_4;
then consider nb being Element of E such that
X3: ( y = v + nb & nb in (- 1) * B ) ;
consider b being Element of E such that
X4: ( nb = (- 1) * b & b in B ) by X3;
reconsider a = y as Element of E by X3;
a + b = (v - b) + b by X3, X4, RLVECT_1:16
.= v by RLVECT_4:1 ;
hence  x in A (+) B by P1, X4, X2; ::_thesis: verum
end;

theorem Th105: :: MORPH_01:8
for E being RealLinearSpace
for A, B being non empty binary-image of E holds A (-) B =  {  v where v is Element of E : v + ((- 1) * B) c= A  }
proof
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) c= A  }
let A, B be non empty binary-image of E; ::_thesis: A (-) B =  {  v where v is Element of E : v + ((- 1) * B) c= A  }
thus  A (-) B c=  {  v where v is Element of E : v + ((- 1) * B) c= A  }  :: according to XBOOLE_0:def_10 ::_thesis:  {  v where v is Element of E : v + ((- 1) * B) c= A  }  c= A (-) B
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A (-) B or x in  {  v where v is Element of E : v + ((- 1) * B) c= A  }  )
assume  x in A (-) B ; ::_thesis: x in  {  v where v is Element of E : v + ((- 1) * B) c= A  }
then consider z being Element of E such that
P1: ( x = z & ( for b being Element of E st b in B holds
z - b in A ) ) ;
 z + ((- 1) * B) c= A
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in z + ((- 1) * B) or y in A )
assume  y in z + ((- 1) * B) ; ::_thesis: y in A
then consider nb being Element of E such that
X1: ( y = z + nb & nb in (- 1) * B ) ;
consider b being Element of E such that
X2: ( nb = (- 1) * b & b in B ) by X1;
 z - b in A by X2, P1;
hence  y in A by X1, X2, RLVECT_1:16; ::_thesis: verum
end;
hence  x in  {  v where v is Element of E : v + ((- 1) * B) c= A  }  by P1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  v where v is Element of E : v + ((- 1) * B) c= A  }  or x in A (-) B )
assume  x in  {  v where v is Element of E : v + ((- 1) * B) c= A  }  ; ::_thesis: x in A (-) B
then consider v being Element of E such that
P1: ( x = v & v + ((- 1) * B) c= A ) ;
 for b being Element of E st b in B holds
v - b in A
proof
let b be Element of E; ::_thesis: ( b in B implies v - b in A )
assume  b in B ; ::_thesis: v - b in A
then  (- 1) * b in (- 1) * B ;
then  v + ((- 1) * b) in v + ((- 1) * B) ;
then  v - b in v + ((- 1) * B) by RLVECT_1:16;
hence  v - b in A by P1; ::_thesis: verum
end;
hence  x in A (-) B by P1; ::_thesis: verum
end;

theorem Th106: :: MORPH_01:9
for E being RealLinearSpace
for A, B being non empty binary-image of E holds
( ( the carrier of E \ A) (+) B = the carrier of E \ (A (-) B) & ( the carrier of E \ A) (-) B = the carrier of E \ (A (+) B) )
proof
let E be RealLinearSpace; ::_thesis: for A, B being non empty binary-image of E holds
( ( the carrier of E \ A) (+) B = the carrier of E \ (A (-) B) & ( the carrier of E \ A) (-) B = the carrier of E \ (A (+) B) )
let A, B be non empty binary-image of E; ::_thesis: ( ( the carrier of E \ A) (+) B = the carrier of E \ (A (-) B) & ( the carrier of E \ A) (-) B = the carrier of E \ (A (+) B) )
percases ( A = the carrier of E or A <> the carrier of E ) ;
supposeX0: A = the carrier of E ; ::_thesis: ( ( the carrier of E \ A) (+) B = the carrier of E \ (A (-) B) & ( the carrier of E \ A) (-) B = the carrier of E \ (A (+) B) )
reconsider X = {} as Subset of E by XBOOLE_1:2;
thus ( the carrier of E \ A) (+) B = X (+) B by X0, XBOOLE_1:37
.= {} by LM0010
.= the carrier of E \ the carrier of E by XBOOLE_1:37
.= the carrier of E \ (A (-) B) by X0, LM0020A ; ::_thesis: ( the carrier of E \ A) (-) B = the carrier of E \ (A (+) B)
thus ( the carrier of E \ A) (-) B = X (-) B by X0, XBOOLE_1:37
.= {} by LM0010A
.= the carrier of E \ the carrier of E by XBOOLE_1:37
.= the carrier of E \ (A (+) B) by X0, LM0020 ; ::_thesis: verum
end;
supposeX0: A <> the carrier of E ; ::_thesis: ( ( the carrier of E \ A) (+) B = the carrier of E \ (A (-) B) & ( the carrier of E \ A) (-) B = the carrier of E \ (A (+) B) )
P1: not the carrier of E \ A is empty
proof
assume  the carrier of E \ A is empty ; ::_thesis: contradiction
then  the carrier of E c= A by XBOOLE_1:37;
hence  contradiction by X0, XBOOLE_0:def_10; ::_thesis: verum
end;
X1: for x being set holds
( x in  {  v where v is Element of E : (v + ((- 1) * B)) /\ ( the carrier of E \ A) <> {}  }  iff ( x in the carrier of E & not x in  {  v where v is Element of E : v + ((- 1) * B) c= A  }  ) )
proof
let x be set ; ::_thesis: ( x in  {  v where v is Element of E : (v + ((- 1) * B)) /\ ( the carrier of E \ A) <> {}  }  iff ( x in the carrier of E & not x in  {  v where v is Element of E : v + ((- 1) * B) c= A  }  ) )
hereby  ::_thesis: ( x in the carrier of E & not x in  {  v where v is Element of E : v + ((- 1) * B) c= A  }  implies x in  {  v where v is Element of E : (v + ((- 1) * B)) /\ ( the carrier of E \ A) <> {}  }  )
assume  x in  {  v where v is Element of E : (v + ((- 1) * B)) /\ ( the carrier of E \ A) <> {}  }  ; ::_thesis: ( x in the carrier of E & not x in  {  w where w is Element of E : w + ((- 1) * B) c= A  }  )
then consider v being Element of E such that
R2: ( x = v & (v + ((- 1) * B)) /\ ( the carrier of E \ A) <> {} ) ;
thus  x in the carrier of E by R2; ::_thesis: not x in  {  w where w is Element of E : w + ((- 1) * B) c= A  }
thus  not x in  {  w where w is Element of E : w + ((- 1) * B) c= A  }  ::_thesis: verum
proof
assume  x in  {  w where w is Element of E : w + ((- 1) * B) c= A  }  ; ::_thesis: contradiction
then consider w being Element of E such that
R4: ( w = x & w + ((- 1) * B) c= A ) ;
 v + ((- 1) * B) misses the carrier of E \ A by R2, R4, XBOOLE_1:85;
hence  contradiction by R2, XBOOLE_0:def_7; ::_thesis: verum
end;
end;
assume X5: ( x in the carrier of E & not x in  {  v where v is Element of E : v + ((- 1) * B) c= A  }  ) ; ::_thesis: x in  {  v where v is Element of E : (v + ((- 1) * B)) /\ ( the carrier of E \ A) <> {}  }
then reconsider w = x as Element of E ;
now__::_thesis:_not_(w_+_((-_1)_*_B))_/\_(_the_carrier_of_E_\_A)_=_{}
assume  (w + ((- 1) * B)) /\ ( the carrier of E \ A) = {} ; ::_thesis: contradiction
then  {} = ((w + ((- 1) * B)) /\ the carrier of E) \ A by XBOOLE_1:49
.= (w + ((- 1) * B)) \ A by XBOOLE_1:28 ;
then  w + ((- 1) * B) c= A by XBOOLE_1:37;
hence  contradiction by X5; ::_thesis: verum
end;
hence  x in  {  v where v is Element of E : (v + ((- 1) * B)) /\ ( the carrier of E \ A) <> {}  }  ; ::_thesis: verum
end;
X2: for x being set holds
( x in  {  v where v is Element of E : v + ((- 1) * B) c= the carrier of E \ A  }  iff ( x in the carrier of E & not x in  {  v where v is Element of E : (v + ((- 1) * B)) /\ A <> {}  }  ) )
proof
let x be set ; ::_thesis: ( x in  {  v where v is Element of E : v + ((- 1) * B) c= the carrier of E \ A  }  iff ( x in the carrier of E & not x in  {  v where v is Element of E : (v + ((- 1) * B)) /\ A <> {}  }  ) )
hereby  ::_thesis: ( x in the carrier of E & not x in  {  v where v is Element of E : (v + ((- 1) * B)) /\ A <> {}  }  implies x in  {  v where v is Element of E : v + ((- 1) * B) c= the carrier of E \ A  }  )
assume  x in  {  v where v is Element of E : v + ((- 1) * B) c= the carrier of E \ A  }  ; ::_thesis: ( x in the carrier of E & not x in  {  w where w is Element of E : (w + ((- 1) * B)) /\ A <> {}  }  )
then consider v being Element of E such that
R2: ( x = v & v + ((- 1) * B) c= the carrier of E \ A ) ;
thus  x in the carrier of E by R2; ::_thesis: not x in  {  w where w is Element of E : (w + ((- 1) * B)) /\ A <> {}  }
thus  not x in  {  w where w is Element of E : (w + ((- 1) * B)) /\ A <> {}  }  ::_thesis: verum
proof
assume  x in  {  w where w is Element of E : (w + ((- 1) * B)) /\ A <> {}  }  ; ::_thesis: contradiction
then consider w being Element of E such that
R4: ( w = x & (w + ((- 1) * B)) /\ A <> {} ) ;
 w + ((- 1) * B) misses the carrier of E \ ( the carrier of E \ A) by R2, R4, XBOOLE_1:85;
then  w + ((- 1) * B) misses the carrier of E /\ A by XBOOLE_1:48;
then  w + ((- 1) * B) misses A by XBOOLE_1:28;
hence  contradiction by R4, XBOOLE_0:def_7; ::_thesis: verum
end;
end;
assume X5: ( x in the carrier of E & not x in  {  v where v is Element of E : (v + ((- 1) * B)) /\ A <> {}  }  ) ; ::_thesis: x in  {  v where v is Element of E : v + ((- 1) * B) c= the carrier of E \ A  }
then reconsider w = x as Element of E ;
reconsider w = x as Element of E by X5;
(w + ((- 1) * B)) \ ( the carrier of E \ A) = ((w + ((- 1) * B)) \ the carrier of E) \/ ((w + ((- 1) * B)) /\ A) by XBOOLE_1:52
.= {} \/ ((w + ((- 1) * B)) /\ A) by XBOOLE_1:37
.= {} by X5 ;
then  w + ((- 1) * B) c= the carrier of E \ A by XBOOLE_1:37;
hence  x in  {  v where v is Element of E : v + ((- 1) * B) c= the carrier of E \ A  }  ; ::_thesis: verum
end;
thus ( the carrier of E \ A) (+) B =  {  v where v is Element of E : (v + ((- 1) * B)) /\ ( the carrier of E \ A) <> {}  }  by Th104, P1
.= the carrier of E \  {  v where v is Element of E : v + ((- 1) * B) c= A  }  by X1, XBOOLE_0:def_5
.= the carrier of E \ (A (-) B) by Th105 ; ::_thesis: ( the carrier of E \ A) (-) B = the carrier of E \ (A (+) B)
thus ( the carrier of E \ A) (-) B =  {  v where v is Element of E : v + ((- 1) * B) c= the carrier of E \ A  }  by Th105, P1
.= the carrier of E \  {  v where v is Element of E : (v + ((- 1) * B)) /\ A <> {}  }  by X2, XBOOLE_0:def_5
.= the carrier of E \ (A (+) B) by Th104 ; ::_thesis: verum
end;
end;
end;

Th107:  for E being non empty Abelian addLoopStr
for A, B being Subset of E holds A (+) B = B (+) A
proof
let E be non empty Abelian addLoopStr ; ::_thesis: for A, B being Subset of E holds A (+) B = B (+) A
let A, B be Subset of E; ::_thesis: A (+) B = B (+) A
thus A (+) B = B + A
.= B (+) A ; ::_thesis: verum
end;

definition
let E be non empty Abelian addLoopStr ;
let A, B be Subset of E;
:: original: +
redefine funcA (+) B ->  Element of K10( the carrier of E);
commutativity
 for A, B being Subset of E holds A + B = B + A by Th107;
end;

theorem Th108A1: :: MORPH_01:10
for E being non empty add-associative addLoopStr
for A, B, C being Subset of E holds (A + B) + C = A + (B + C)
proof
let E be non empty add-associative addLoopStr ; ::_thesis: for A, B, C being Subset of E holds (A + B) + C = A + (B + C)
let A, B, C be Subset of E; ::_thesis: (A + B) + C = A + (B + C)
 for x being Element of E holds
( x in (A + B) + C iff x in A + (B + C) )
proof
let x be Element of E; ::_thesis: ( x in (A + B) + C iff x in A + (B + C) )
hereby  ::_thesis: ( x in A + (B + C) implies x in (A + B) + C )
assume  x in (A + B) + C ; ::_thesis: x in A + (B + C)
then consider ab, c being Element of E such that
P1: ( x = ab + c & ab in A + B & c in C ) ;
consider a, b being Element of E such that
P2: ( ab = a + b & a in A & b in B ) by P1;
P3: x = a + (b + c) by P1, P2, RLVECT_1:def_3;
 b + c in B + C by P1, P2;
hence  x in A + (B + C) by P2, P3; ::_thesis: verum
end;
assume  x in A + (B + C) ; ::_thesis: x in (A + B) + C
then consider a, bc being Element of E such that
P1: ( x = a + bc & a in A & bc in B + C ) ;
consider b, c being Element of E such that
P2: ( bc = b + c & b in B & c in C ) by P1;
P3: x = (a + b) + c by P1, P2, RLVECT_1:def_3;
 a + b in A + B by P1, P2;
hence  x in (A + B) + C by P2, P3; ::_thesis: verum
end;
hence  (A + B) + C = A + (B + C) by SUBSET_1:3; ::_thesis: verum
end;

theorem :: MORPH_01:11
for E being RealLinearSpace
for A, B, C being non empty binary-image of E holds (A (+) B) (+) C = A (+) (B (+) C) by Th108A1;

theorem Th108B: :: MORPH_01:12
for E being RealLinearSpace
for F being binary-image-family of E
for B being non empty binary-image of E holds (union F) (+) B = union  {  (X (+) B) where X is binary-image of E : X in F  }
proof
let E be RealLinearSpace; ::_thesis: for F being binary-image-family of E
for B being non empty binary-image of E holds (union F) (+) B = union  {  (X (+) B) where X is binary-image of E : X in F  }
let F be binary-image-family of E; ::_thesis: for B being non empty binary-image of E holds (union F) (+) B = union  {  (X (+) B) where X is binary-image of E : X in F  }
let B be non empty binary-image of E; ::_thesis: (union F) (+) B = union  {  (X (+) B) where X is binary-image of E : X in F  }
 for x being set holds
( x in (union F) (+) B iff x in union  {  (X (+) B) where X is binary-image of E : X in F  }  )
proof
let x be set ; ::_thesis: ( x in (union F) (+) B iff x in union  {  (X (+) B) where X is binary-image of E : X in F  }  )
hereby  ::_thesis: ( x in union  {  (X (+) B) where X is binary-image of E : X in F  }  implies x in (union F) (+) B )
assume  x in (union F) (+) B ; ::_thesis: x in union  {  (W (+) B) where W is binary-image of E : W in F  }
then consider f, b being Element of E such that
P1: ( x = f + b & f in union F & b in B ) ;
consider Y being set  such that
P2: ( f in Y & Y in F ) by P1, TARSKI:def_4;
reconsider X = Y as binary-image of E by P2;
P3: x in X (+) B by P1, P2;
 X (+) B in  {  (W (+) B) where W is binary-image of E : W in F  }  by P2;
hence  x in union  {  (W (+) B) where W is binary-image of E : W in F  }  by P3, TARSKI:def_4; ::_thesis: verum
end;
assume  x in union  {  (X (+) B) where X is binary-image of E : X in F  }  ; ::_thesis: x in (union F) (+) B
then consider Y being set  such that
P1: ( x in Y & Y in  {  (X (+) B) where X is binary-image of E : X in F  }  ) by TARSKI:def_4;
consider W being binary-image of E such that
P2: ( Y = W (+) B & W in F ) by P1;
consider f, b being Element of E such that
P3: ( x = f + b & f in W & b in B ) by P1, P2;
 W c= union F by P2, ZFMISC_1:74;
hence  x in (union F) (+) B by P3; ::_thesis: verum
end;
hence  (union F) (+) B = union  {  (X (+) B) where X is binary-image of E : X in F  }  by TARSKI:1; ::_thesis: verum
end;

theorem :: MORPH_01:13
for E being RealLinearSpace
for F being binary-image-family of E
for A being non empty binary-image of E holds A (+) (union F) = union  {  (A (+) X) where X is binary-image of E : X in F  }
proof
let E be RealLinearSpace; ::_thesis: for F being binary-image-family of E
for A being non empty binary-image of E holds A (+) (union F) = union  {  (A (+) X) where X is binary-image of E : X in F  }
let F be binary-image-family of E; ::_thesis: for A being non empty binary-image of E holds A (+) (union F) = union  {  (A (+) X) where X is binary-image of E : X in F  }
let A be non empty binary-image of E; ::_thesis: A (+) (union F) = union  {  (A (+) X) where X is binary-image of E : X in F  }
P1: for x being set holds
( x in  {  (X (+) A) where X is binary-image of E : X in F  }  iff x in  {  (A (+) X) where X is binary-image of E : X in F  }  )
proof
let x be set ; ::_thesis: ( x in  {  (X (+) A) where X is binary-image of E : X in F  }  iff x in  {  (A (+) X) where X is binary-image of E : X in F  }  )
hereby  ::_thesis: ( x in  {  (A (+) X) where X is binary-image of E : X in F  }  implies x in  {  (X (+) A) where X is binary-image of E : X in F  }  )
assume  x in  {  (X (+) A) where X is binary-image of E : X in F  }  ; ::_thesis: x in  {  (A (+) X) where X is binary-image of E : X in F  }
then consider W being binary-image of E such that
X1: ( x = W (+) A & W in F ) ;
 ( x = A (+) W & W in F ) by X1;
hence  x in  {  (A (+) X) where X is binary-image of E : X in F  }  ; ::_thesis: verum
end;
assume  x in  {  (A (+) X) where X is binary-image of E : X in F  }  ; ::_thesis: x in  {  (X (+) A) where X is binary-image of E : X in F  }
then consider W being binary-image of E such that
X1: ( x = A (+) W & W in F ) ;
 ( x = W (+) A & W in F ) by X1;
hence  x in  {  (X (+) A) where X is binary-image of E : X in F  }  ; ::_thesis: verum
end;
thus A (+) (union F) = (union F) (+) A
.= union  {  (X (+) A) where X is binary-image of E : X in F  }  by Th108B
.= union  {  (A (+) X) where X is binary-image of E : X in F  }  by P1, TARSKI:1 ; ::_thesis: verum
end;

theorem Th110: :: MORPH_01:14
for E being RealLinearSpace
for F being binary-image-family of E
for B being non empty binary-image of E holds (meet F) (+) B c= meet  {  (X (+) B) where X is binary-image of E : X in F  }
proof
let E be RealLinearSpace; ::_thesis: for F being binary-image-family of E
for B being non empty binary-image of E holds (meet F) (+) B c= meet  {  (X (+) B) where X is binary-image of E : X in F  }
let F be binary-image-family of E; ::_thesis: for B being non empty binary-image of E holds (meet F) (+) B c= meet  {  (X (+) B) where X is binary-image of E : X in F  }
let B be non empty binary-image of E; ::_thesis: (meet F) (+) B c= meet  {  (X (+) B) where X is binary-image of E : X in F  }
percases ( F = {} or F <> {} ) ;
supposeG1: F = {} ; ::_thesis: (meet F) (+) B c= meet  {  (X (+) B) where X is binary-image of E : X in F  }
reconsider Z = meet F as Subset of E ;
 meet F = {} by G1, SETFAM_1:def_1;
then  Z (+) B = {} by LM0010;
hence  (meet F) (+) B c= meet  {  (X (+) B) where X is binary-image of E : X in F  }  by XBOOLE_1:2; ::_thesis: verum
end;
suppose F <> {} ; ::_thesis: (meet F) (+) B c= meet  {  (X (+) B) where X is binary-image of E : X in F  }
then consider W0 being set  such that
P0: W0 in F by XBOOLE_0:def_1;
reconsider W0 = W0 as binary-image of E by P0;
P2: W0 (+) B in  {  (W (+) B) where W is binary-image of E : W in F  }  by P0;
now__::_thesis:_for_x_being_set_st_x_in_(meet_F)_(+)_B_holds_
x_in_meet__{__(W_(+)_B)_where_W_is_binary-image_of_E_:_W_in_F__}_
let x be set ; ::_thesis: ( x in (meet F) (+) B implies x in meet  {  (W (+) B) where W is binary-image of E : W in F  }  )
assume  x in (meet F) (+) B ; ::_thesis: x in meet  {  (W (+) B) where W is binary-image of E : W in F  }
then consider f, b being Element of E such that
P1: ( x = f + b & f in meet F & b in B ) ;
now__::_thesis:_for_Y_being_set_st_Y_in__{__(X_(+)_B)_where_X_is_binary-image_of_E_:_X_in_F__}__holds_
x_in_Y
let Y be set ; ::_thesis: ( Y in  {  (X (+) B) where X is binary-image of E : X in F  }  implies x in Y )
assume  Y in  {  (X (+) B) where X is binary-image of E : X in F  }  ; ::_thesis: x in Y
then consider X being binary-image of E such that
P3: ( Y = X (+) B & X in F ) ;
 meet F c= X by P3, SETFAM_1:3;
hence  x in Y by P1, P3; ::_thesis: verum
end;
hence  x in meet  {  (W (+) B) where W is binary-image of E : W in F  }  by P2, SETFAM_1:def_1; ::_thesis: verum
end;
hence  (meet F) (+) B c= meet  {  (X (+) B) where X is binary-image of E : X in F  }  by TARSKI:def_3; ::_thesis: verum
end;
end;
end;

theorem :: MORPH_01:15
for E being RealLinearSpace
for F being binary-image-family of E
for A being non empty binary-image of E holds A (+) (meet F) c= meet  {  (A (+) X) where X is binary-image of E : X in F  }
proof
let E be RealLinearSpace; ::_thesis: for F being binary-image-family of E
for A being non empty binary-image of E holds A (+) (meet F) c= meet  {  (A (+) X) where X is binary-image of E : X in F  }
let F be binary-image-family of E; ::_thesis: for A being non empty binary-image of E holds A (+) (meet F) c= meet  {  (A (+) X) where X is binary-image of E : X in F  }
let A be non empty binary-image of E; ::_thesis: A (+) (meet F) c= meet  {  (A (+) X) where X is binary-image of E : X in F  }
P1: for x being set holds
( x in  {  (X (+) A) where X is binary-image of E : X in F  }  iff x in  {  (A (+) X) where X is binary-image of E : X in F  }  )
proof
let x be set ; ::_thesis: ( x in  {  (X (+) A) where X is binary-image of E : X in F  }  iff x in  {  (A (+) X) where X is binary-image of E : X in F  }  )
hereby  ::_thesis: ( x in  {  (A (+) X) where X is binary-image of E : X in F  }  implies x in  {  (X (+) A) where X is binary-image of E : X in F  }  )
assume  x in  {  (X (+) A) where X is binary-image of E : X in F  }  ; ::_thesis: x in  {  (A (+) X) where X is binary-image of E : X in F  }
then consider W being binary-image of E such that
X1: ( x = W (+) A & W in F ) ;
 ( x = A (+) W & W in F ) by X1;
hence  x in  {  (A (+) X) where X is binary-image of E : X in F  }  ; ::_thesis: verum
end;
assume  x in  {  (A (+) X) where X is binary-image of E : X in F  }  ; ::_thesis: x in  {  (X (+) A) where X is binary-image of E : X in F  }
then consider W being binary-image of E such that
X1: ( x = A (+) W & W in F ) ;
 ( x = W (+) A & W in F ) by X1;
hence  x in  {  (X (+) A) where X is binary-image of E : X in F  }  ; ::_thesis: verum
end;
 A (+) (meet F) c= meet  {  (X (+) A) where X is binary-image of E : X in F  }  by Th110;
hence  A (+) (meet F) c= meet  {  (A (+) X) where X is binary-image of E : X in F  }  by P1, TARSKI:1; ::_thesis: verum
end;

theorem Th112: :: MORPH_01:16
for E being non empty addLoopStr
for A, B, C being Subset of E st B c= C holds
A + B c= A + C
proof
let E be non empty addLoopStr ; ::_thesis: for A, B, C being Subset of E st B c= C holds
A + B c= A + C
let A, B, C be Subset of E; ::_thesis: ( B c= C implies A + B c= A + C )
assume AS1: B c= C ; ::_thesis: A + B c= A + C
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A + B or x in A + C )
assume  x in A + B ; ::_thesis: x in A + C
then consider a, b being Element of E such that
P1: ( x = a + b & a in A & b in B ) ;
thus  x in A + C by AS1, P1; ::_thesis: verum
end;

theorem Th113: :: MORPH_01:17
for E being RealLinearSpace
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) )
proof
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 set holds
( x in (v + A) (+) B iff x in A (+) (v + B) )
proof
let x be set ; ::_thesis: ( x in (v + A) (+) B iff x in A (+) (v + B) )
hereby  ::_thesis: ( x in A (+) (v + B) implies x in (v + A) (+) B )
assume  x in (v + A) (+) B ; ::_thesis: x in A (+) (v + B)
then consider f, b being Element of E such that
P1: ( x = f + b & f in v + A & b in B ) ;
consider a being Element of E such that
P2: ( f = v + a & a in A ) by P1;
P3: x = a + (v + b) by P1, P2, RLVECT_1:def_3;
 v + b in v + B by P1;
hence  x in A (+) (v + B) by P3, P2; ::_thesis: verum
end;
assume  x in A (+) (v + B) ; ::_thesis: x in (v + A) (+) B
then consider a, f being Element of E such that
P1: ( x = a + f & a in A & f in v + B ) ;
consider b being Element of E such that
P2: ( f = v + b & b in B ) by P1;
P3: x = (v + a) + b by P1, P2, RLVECT_1:def_3;
 v + a in v + A by P1;
hence  x in (v + A) (+) B by P3, P2; ::_thesis: verum
end;
hence  (v + A) (+) B = A (+) (v + B) by TARSKI:1; ::_thesis: (v + A) (+) B = v + (A (+) B)
 for x being set holds
( x in (v + A) (+) B iff x in v + (A (+) B) )
proof
let x be set ; ::_thesis: ( x in (v + A) (+) B iff x in v + (A (+) B) )
hereby  ::_thesis: ( x in v + (A (+) B) implies x in (v + A) (+) B )
assume  x in (v + A) (+) B ; ::_thesis: x in v + (A (+) B)
then consider f, b being Element of E such that
P1: ( x = f + b & f in v + A & b in B ) ;
consider a being Element of E such that
P2: ( f = v + a & a in A ) by P1;
P3: x = v + (a + b) by P1, P2, RLVECT_1:def_3;
 a + b in A + B by P1, P2;
hence  x in v + (A (+) B) by P3; ::_thesis: verum
end;
assume  x in v + (A (+) B) ; ::_thesis: x in (v + A) (+) B
then consider ab being Element of E such that
P1: ( x = v + ab & ab in A (+) B ) ;
consider a, b being Element of E such that
P2: ( ab = a + b & a in A & b in B ) by P1;
P3: x = (v + a) + b by P1, P2, RLVECT_1:def_3;
 v + a in v + A by P2;
hence  x in (v + A) (+) B by P3, P2; ::_thesis: verum
end;
hence  (v + A) (+) B = v + (A (+) B) by TARSKI:1; ::_thesis: verum
end;

theorem Th114: :: MORPH_01:18
for E being RealLinearSpace
for F being binary-image-family of E
for B being non empty binary-image of E holds (meet F) (-) B = meet  {  (X (-) B) where X is binary-image of E : X in F  }
proof
let E be RealLinearSpace; ::_thesis: for F being binary-image-family of E
for B being non empty binary-image of E holds (meet F) (-) B = meet  {  (X (-) B) where X is binary-image of E : X in F  }
let F be binary-image-family of E; ::_thesis: for B being non empty binary-image of E holds (meet F) (-) B = meet  {  (X (-) B) where X is binary-image of E : X in F  }
let B be non empty binary-image of E; ::_thesis: (meet F) (-) B = meet  {  (X (-) B) where X is binary-image of E : X in F  }
percases ( F = {} or F <> {} ) ;
supposeG1: F = {} ; ::_thesis: (meet F) (-) B = meet  {  (X (-) B) where X is binary-image of E : X in F  }
reconsider Z = meet F as Subset of E ;
G2: meet F = {} by G1, SETFAM_1:def_1;
  {  (X (-) B) where X is binary-image of E : X in F  }  = {}
proof
assume   {  (X (-) B) where X is binary-image of E : X in F  }  <> {} ; ::_thesis: contradiction
then consider x being set  such that
S1: x in  {  (X (-) B) where X is binary-image of E : X in F  }  by XBOOLE_0:def_1;
 ex X being binary-image of E st
( x = X (-) B & X in F ) by S1;
hence  contradiction by G1; ::_thesis: verum
end;
then  {} = meet  {  (X (-) B) where X is binary-image of E : X in F  }  by SETFAM_1:def_1;
hence  (meet F) (-) B = meet  {  (X (-) B) where X is binary-image of E : X in F  }  by G2, LM0010A; ::_thesis: verum
end;
supposeG2: F <> {} ; ::_thesis: (meet F) (-) B = meet  {  (X (-) B) where X is binary-image of E : X in F  }
then consider W0 being set  such that
P0: W0 in F by XBOOLE_0:def_1;
reconsider W0 = W0 as binary-image of E by P0;
P2: W0 (-) B in  {  (W (-) B) where W is binary-image of E : W in F  }  by P0;
 for x being set holds
( x in (meet F) (-) B iff x in meet  {  (W (-) B) where W is binary-image of E : W in F  }  )
proof
let x be set ; ::_thesis: ( x in (meet F) (-) B iff x in meet  {  (W (-) B) where W is binary-image of E : W in F  }  )
hereby  ::_thesis: ( x in meet  {  (W (-) B) where W is binary-image of E : W in F  }  implies x in (meet F) (-) B )
assume  x in (meet F) (-) B ; ::_thesis: x in meet  {  (W (-) B) where W is binary-image of E : W in F  }
then consider z being Element of E such that
Q1: ( x = z & ( for b being Element of E st b in B holds
z - b in meet F ) ) ;
now__::_thesis:_for_Y_being_set_st_Y_in__{__(X_(-)_B)_where_X_is_binary-image_of_E_:_X_in_F__}__holds_
x_in_Y
let Y be set ; ::_thesis: ( Y in  {  (X (-) B) where X is binary-image of E : X in F  }  implies x in Y )
assume  Y in  {  (X (-) B) where X is binary-image of E : X in F  }  ; ::_thesis: x in Y
then consider X being binary-image of E such that
P3: ( Y = X (-) B & X in F ) ;
now__::_thesis:_for_b_being_Element_of_E_st_b_in_B_holds_
z_-_b_in_X
let b be Element of E; ::_thesis: ( b in B implies z - b in X )
assume  b in B ; ::_thesis: z - b in X
then X1: z - b in meet F by Q1;
 meet F c= X by P3, SETFAM_1:3;
hence  z - b in X by X1; ::_thesis: verum
end;
hence  x in Y by P3, Q1; ::_thesis: verum
end;
hence  x in meet  {  (W (-) B) where W is binary-image of E : W in F  }  by P2, SETFAM_1:def_1; ::_thesis: verum
end;
assume X1: x in meet  {  (W (-) B) where W is binary-image of E : W in F  }  ; ::_thesis: x in (meet F) (-) B
Q1: for W being binary-image of E st W in F holds
x in W (-) B
proof
let W be binary-image of E; ::_thesis: ( W in F implies x in W (-) B )
assume  W in F ; ::_thesis: x in W (-) B
then  W (-) B in  {  (D (-) B) where D is binary-image of E : D in F  }  ;
hence  x in W (-) B by X1, SETFAM_1:def_1; ::_thesis: verum
end;
 x in W0 (-) B by P0, Q1;
then reconsider z = x as Element of E ;
 for b being Element of E st b in B holds
z - b in meet F
proof
assume  ex b being Element of E st
( b in B & not z - b in meet F ) ; ::_thesis: contradiction
then consider b being Element of E such that
D2: ( b in B & not z - b in meet F ) ;
consider X being set  such that
Q5: ( X in F & not z - b in X ) by G2, D2, SETFAM_1:def_1;
reconsider X = X as binary-image of E by Q5;
 z in X (-) B by Q5, Q1;
then consider zz being Element of E such that
Q70: ( z = zz & ( for b being Element of E st b in B holds
zz - b in X ) ) ;
thus  contradiction by Q70, D2, Q5; ::_thesis: verum
end;
hence  x in (meet F) (-) B ; ::_thesis: verum
end;
hence  (meet F) (-) B = meet  {  (X (-) B) where X is binary-image of E : X in F  }  by TARSKI:1; ::_thesis: verum
end;
end;
end;

theorem :: MORPH_01:19
for E being RealLinearSpace
for F being binary-image-family of E
for B being non empty binary-image of E holds meet  {  (B (-) X) where X is binary-image of E : X in F  }  c= B (-) (meet F)
proof
let E be RealLinearSpace; ::_thesis: for F being binary-image-family of E
for B being non empty binary-image of E holds meet  {  (B (-) X) where X is binary-image of E : X in F  }  c= B (-) (meet F)
let F be binary-image-family of E; ::_thesis: for B being non empty binary-image of E holds meet  {  (B (-) X) where X is binary-image of E : X in F  }  c= B (-) (meet F)
let B be non empty binary-image of E; ::_thesis: meet  {  (B (-) X) where X is binary-image of E : X in F  }  c= B (-) (meet F)
percases ( F = {} or F <> {} ) ;
supposeG1: F = {} ; ::_thesis: meet  {  (B (-) X) where X is binary-image of E : X in F  }  c= B (-) (meet F)
reconsider Z = meet F as Subset of E ;
  {  (B (-) X) where X is binary-image of E : X in F  }  = {}
proof
assume   {  (B (-) X) where X is binary-image of E : X in F  }  <> {} ; ::_thesis: contradiction
then consider x being set  such that
S1: x in  {  (B (-) X) where X is binary-image of E : X in F  }  by XBOOLE_0:def_1;
 ex X being binary-image of E st
( x = B (-) X & X in F ) by S1;
hence  contradiction by G1; ::_thesis: verum
end;
then  {} = meet  {  (B (-) X) where X is binary-image of E : X in F  }  by SETFAM_1:def_1;
hence  meet  {  (B (-) X) where X is binary-image of E : X in F  }  c= B (-) (meet F) by XBOOLE_1:2; ::_thesis: verum
end;
suppose F <> {} ; ::_thesis: meet  {  (B (-) X) where X is binary-image of E : X in F  }  c= B (-) (meet F)
then consider W0 being set  such that
P0: W0 in F by XBOOLE_0:def_1;
reconsider W0 = W0 as binary-image of E by P0;
 for x being set st x in meet  {  (B (-) W) where W is binary-image of E : W in F  }  holds
x in B (-) (meet F)
proof
let x be set ; ::_thesis: ( x in meet  {  (B (-) W) where W is binary-image of E : W in F  }  implies x in B (-) (meet F) )
assume X1: x in meet  {  (B (-) W) where W is binary-image of E : W in F  }  ; ::_thesis: x in B (-) (meet F)
Q1: for W being binary-image of E st W in F holds
x in B (-) W
proof
let W be binary-image of E; ::_thesis: ( W in F implies x in B (-) W )
assume  W in F ; ::_thesis: x in B (-) W
then  B (-) W in  {  (B (-) D) where D is binary-image of E : D in F  }  ;
hence  x in B (-) W by X1, SETFAM_1:def_1; ::_thesis: verum
end;
T1: x in B (-) W0 by P0, Q1;
then reconsider z = x as Element of E ;
 for f being Element of E st f in meet F holds
z - f in B
proof
let f be Element of E; ::_thesis: ( f in meet F implies z - f in B )
assume D1: f in meet F ; ::_thesis: z - f in B
D2: meet F c= W0 by P0, SETFAM_1:3;
consider zz being Element of E such that
Q7: ( z = zz & ( for w being Element of E st w in W0 holds
zz - w in B ) ) by T1;
thus  z - f in B by Q7, D1, D2; ::_thesis: verum
end;
hence  x in B (-) (meet F) ; ::_thesis: verum
end;
hence  meet  {  (B (-) X) where X is binary-image of E : X in F  }  c= B (-) (meet F) by TARSKI:def_3; ::_thesis: verum
end;
end;
end;

theorem :: MORPH_01:20
for E being RealLinearSpace
for F being binary-image-family of E
for B being non empty binary-image of E holds union  {  (X (-) B) where X is binary-image of E : X in F  }  c= (union F) (-) B
proof
let E be RealLinearSpace; ::_thesis: for F being binary-image-family of E
for B being non empty binary-image of E holds union  {  (X (-) B) where X is binary-image of E : X in F  }  c= (union F) (-) B
let F be binary-image-family of E; ::_thesis: for B being non empty binary-image of E holds union  {  (X (-) B) where X is binary-image of E : X in F  }  c= (union F) (-) B
let B be non empty binary-image of E; ::_thesis: union  {  (X (-) B) where X is binary-image of E : X in F  }  c= (union F) (-) B
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union  {  (X (-) B) where X is binary-image of E : X in F  }  or x in (union F) (-) B )
assume  x in union  {  (X (-) B) where X is binary-image of E : X in F  }  ; ::_thesis: x in (union F) (-) B
then consider Y being set  such that
P1: ( x in Y & Y in  {  (X (-) B) where X is binary-image of E : X in F  }  ) by TARSKI:def_4;
consider W being binary-image of E such that
P2: ( Y = W (-) B & W in F ) by P1;
consider z being Element of E such that
Q7: ( x = z & ( for b being Element of E st b in B holds
z - b in W ) ) by P1, P2;
now__::_thesis:_for_b_being_Element_of_E_st_b_in_B_holds_
z_-_b_in_union_F
let b be Element of E; ::_thesis: ( b in B implies z - b in union F )
assume  b in B ; ::_thesis: z - b in union F
then X2: z - b in W by Q7;
 W c= union F by P2, ZFMISC_1:74;
hence  z - b in union F by X2; ::_thesis: verum
end;
hence  x in (union F) (-) B by Q7; ::_thesis: verum
end;

theorem :: MORPH_01:21
for E being RealLinearSpace
for F being binary-image-family of E
for B being non empty binary-image of E st F <> {} holds
B (-) (union F) = meet  {  (B (-) X) where X is binary-image of E : X in F  }
proof
let E be RealLinearSpace; ::_thesis: for F being binary-image-family of E
for B being non empty binary-image of E st F <> {} holds
B (-) (union F) = meet  {  (B (-) X) where X is binary-image of E : X in F  }
let F be binary-image-family of E; ::_thesis: for B being non empty binary-image of E st F <> {} holds
B (-) (union F) = meet  {  (B (-) X) where X is binary-image of E : X in F  }
let B be non empty binary-image of E; ::_thesis: ( F <> {} implies B (-) (union F) = meet  {  (B (-) X) where X is binary-image of E : X in F  }  )
assume  F <> {} ; ::_thesis: B (-) (union F) = meet  {  (B (-) X) where X is binary-image of E : X in F  }
then consider W0 being set  such that
P0: W0 in F by XBOOLE_0:def_1;
reconsider W0 = W0 as binary-image of E by P0;
P2: B (-) W0 in  {  (B (-) X) where X is binary-image of E : X in F  }  by P0;
 for x being set holds
( x in B (-) (union F) iff x in meet  {  (B (-) X) where X is binary-image of E : X in F  }  )
proof
let x be set ; ::_thesis: ( x in B (-) (union F) iff x in meet  {  (B (-) X) where X is binary-image of E : X in F  }  )
hereby  ::_thesis: ( x in meet  {  (B (-) X) where X is binary-image of E : X in F  }  implies x in B (-) (union F) )
assume  x in B (-) (union F) ; ::_thesis: x in meet  {  (B (-) W) where W is binary-image of E : W in F  }
then consider z being Element of E such that
Q1: ( x = z & ( for f being Element of E st f in union F holds
z - f in B ) ) ;
now__::_thesis:_for_Y_being_set_st_Y_in__{__(B_(-)_X)_where_X_is_binary-image_of_E_:_X_in_F__}__holds_
x_in_Y
let Y be set ; ::_thesis: ( Y in  {  (B (-) X) where X is binary-image of E : X in F  }  implies x in Y )
assume  Y in  {  (B (-) X) where X is binary-image of E : X in F  }  ; ::_thesis: x in Y
then consider X being binary-image of E such that
Q2: ( Y = B (-) X & X in F ) ;
now__::_thesis:_for_f_being_Element_of_E_st_f_in_X_holds_
z_-_f_in_B
let f be Element of E; ::_thesis: ( f in X implies z - f in B )
assume  f in X ; ::_thesis: z - f in B
then  f in union F by Q2, TARSKI:def_4;
hence  z - f in B by Q1; ::_thesis: verum
end;
hence  x in Y by Q1, Q2; ::_thesis: verum
end;
hence  x in meet  {  (B (-) W) where W is binary-image of E : W in F  }  by P2, SETFAM_1:def_1; ::_thesis: verum
end;
assume X1: x in meet  {  (B (-) W) where W is binary-image of E : W in F  }  ; ::_thesis: x in B (-) (union F)
Q1: for W being binary-image of E st W in F holds
x in B (-) W
proof
let W be binary-image of E; ::_thesis: ( W in F implies x in B (-) W )
assume  W in F ; ::_thesis: x in B (-) W
then  B (-) W in  {  (B (-) D) where D is binary-image of E : D in F  }  ;
hence  x in B (-) W by X1, SETFAM_1:def_1; ::_thesis: verum
end;
 x in B (-) W0 by P0, Q1;
then reconsider z = x as Element of E ;
 for f being Element of E st f in union F holds
z - f in B
proof
let f be Element of E; ::_thesis: ( f in union F implies z - f in B )
assume  f in union F ; ::_thesis: z - f in B
then consider W being set  such that
Q4: ( f in W & W in F ) by TARSKI:def_4;
reconsider W = W as binary-image of E by Q4;
 z in B (-) W by Q1, Q4;
then consider w being Element of E such that
Q7: ( z = w & ( for f being Element of E st f in W holds
w - f in B ) ) ;
thus  z - f in B by Q4, Q7; ::_thesis: verum
end;
hence  x in B (-) (union F) ; ::_thesis: verum
end;
hence  B (-) (union F) = meet  {  (B (-) X) where X is binary-image of E : X in F  }  by TARSKI:1; ::_thesis: verum
end;

theorem Th118: :: MORPH_01:22
for E being RealLinearSpace
for A, B, C being non empty binary-image of E st A c= B holds
A (-) C c= B (-) C
proof
let E be RealLinearSpace; ::_thesis: for A, B, C being non empty binary-image of E st A c= B holds
A (-) C c= B (-) C
let A, B, C be non empty binary-image of E; ::_thesis: ( A c= B implies A (-) C c= B (-) C )
assume AS: A c= B ; ::_thesis: A (-) C c= B (-) C
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A (-) C or x in B (-) C )
assume  x in A (-) C ; ::_thesis: x in B (-) C
then consider w being Element of E such that
P2: ( x = w & ( for c being Element of E st c in C holds
w - c in A ) ) ;
now__::_thesis:_for_c_being_Element_of_E_st_c_in_C_holds_
w_-_c_in_B
let c be Element of E; ::_thesis: ( c in C implies w - c in B )
assume  c in C ; ::_thesis: w - c in B
then  w - c in A by P2;
hence  w - c in B by AS; ::_thesis: verum
end;
hence  x in B (-) C by P2; ::_thesis: verum
end;

theorem :: MORPH_01:23
for E being RealLinearSpace
for A, B, C being non empty binary-image of E st A c= B holds
C (-) B c= C (-) A
proof
let E be RealLinearSpace; ::_thesis: for A, B, C being non empty binary-image of E st A c= B holds
C (-) B c= C (-) A
let A, B, C be non empty binary-image of E; ::_thesis: ( A c= B implies C (-) B c= C (-) A )
assume AS: A c= B ; ::_thesis: C (-) B c= C (-) A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in C (-) B or x in C (-) A )
assume  x in C (-) B ; ::_thesis: x in C (-) A
then consider w being Element of E such that
P2: ( x = w & ( for b being Element of E st b in B holds
w - b in C ) ) ;
 for a being Element of E st a in A holds
w - a in C by AS, P2;
hence  x in C (-) A by P2; ::_thesis: verum
end;

theorem Th120: :: MORPH_01:24
for E being RealLinearSpace
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) )
proof
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 set holds
( x in (v + A) (-) B iff x in A (-) (v + B) )
proof
let x be set ; ::_thesis: ( x in (v + A) (-) B iff x in A (-) (v + B) )
hereby  ::_thesis: ( x in A (-) (v + B) implies x in (v + A) (-) B )
assume  x in (v + A) (-) B ; ::_thesis: x in A (-) (v + B)
then consider w being Element of E such that
P1: ( x = w & ( for b being Element of E st b in B holds
w - b in v + A ) ) ;
now__::_thesis:_for_vb_being_Element_of_E_st_vb_in_v_+_B_holds_
w_-_vb_in_A
let vb be Element of E; ::_thesis: ( vb in v + B implies w - vb in A )
assume  vb in v + B ; ::_thesis: w - vb in A
then consider b being Element of E such that
P3: ( vb = v + b & b in B ) ;
 w - b in v + A by P3, P1;
then consider a being Element of E such that
P5: ( w - b = v + a & a in A ) ;
w - vb = (w - b) - v by P3, RLVECT_1:27
.= a by P5, RLVECT_4:1 ;
hence  w - vb in A by P5; ::_thesis: verum
end;
hence  x in A (-) (v + B) by P1; ::_thesis: verum
end;
assume  x in A (-) (v + B) ; ::_thesis: x in (v + A) (-) B
then consider w being Element of E such that
P1: ( x = w & ( for vb being Element of E st vb in v + B holds
w - vb in A ) ) ;
now__::_thesis:_for_b_being_Element_of_E_st_b_in_B_holds_
w_-_b_in_v_+_A
let b be Element of E; ::_thesis: ( b in B implies w - b in v + A )
assume  b in B ; ::_thesis: w - b in v + A
then  v + b in v + B ;
then  w - (v + b) in A by P1;
then P4: v + (w - (v + b)) in v + A ;
v + (w - (v + b)) = (v + w) - (v + b) by RLVECT_1:28
.= w + (v - (v + b)) by RLVECT_1:28
.= w + ((v - v) - b) by RLVECT_1:27
.= w + ((0. E) - b) by RLVECT_1:15 ;
hence  w - b in v + A by RLVECT_1:14, P4; ::_thesis: verum
end;
hence  x in (v + A) (-) B by P1; ::_thesis: verum
end;
hence  (v + A) (-) B = A (-) (v + B) by TARSKI:1; ::_thesis: (v + A) (-) B = v + (A (-) B)
 for x being set holds
( x in (v + A) (-) B iff x in v + (A (-) B) )
proof
let x be set ; ::_thesis: ( x in (v + A) (-) B iff x in v + (A (-) B) )
hereby  ::_thesis: ( x in v + (A (-) B) implies x in (v + A) (-) B )
assume  x in (v + A) (-) B ; ::_thesis: x in v + (A (-) B)
then consider w being Element of E such that
P1: ( x = w & ( for b being Element of E st b in B holds
w - b in v + A ) ) ;
now__::_thesis:_for_b_being_Element_of_E_st_b_in_B_holds_
(w_-_v)_-_b_in_A
let b be Element of E; ::_thesis: ( b in B implies (w - v) - b in A )
assume  b in B ; ::_thesis: (w - v) - b in A
then X2: w - b in v + A by P1;
consider a being Element of E such that
X3: ( w - b = v + a & a in A ) by X2;
(w - v) - b = w - (v + b) by RLVECT_1:27
.= (v + a) - v by RLVECT_1:27, X3
.= a by RLVECT_4:1 ;
hence  (w - v) - b in A by X3; ::_thesis: verum
end;
then X4: w - v in A (-) B ;
 v + (w - v) = w by RLVECT_4:1;
hence  x in v + (A (-) B) by P1, X4; ::_thesis: verum
end;
assume  x in v + (A (-) B) ; ::_thesis: x in (v + A) (-) B
then consider ab being Element of E such that
X1: ( x = v + ab & ab in A (-) B ) ;
reconsider w = x as Element of E by X1;
consider d being Element of E such that
Y1: ( ab = d & ( for b being Element of E st b in B holds
d - b in A ) ) by X1;
now__::_thesis:_for_b_being_Element_of_E_st_b_in_B_holds_
(v_+_ab)_-_b_in_v_+_A
let b be Element of E; ::_thesis: ( b in B implies (v + ab) - b in v + A )
assume  b in B ; ::_thesis: (v + ab) - b in v + A
then X2: ab - b in A by Y1;
 (v + ab) - b = v + (ab - b) by RLVECT_1:28;
hence  (v + ab) - b in v + A by X2; ::_thesis: verum
end;
hence  x in (v + A) (-) B by X1; ::_thesis: verum
end;
hence  (v + A) (-) B = v + (A (-) B) by TARSKI:1; ::_thesis: verum
end;

theorem Th121: :: MORPH_01:25
for E being RealLinearSpace
for A, B, C being non empty binary-image of E holds (A (-) B) (-) C = A (-) (B (+) C)
proof
let E be RealLinearSpace; ::_thesis: for A, B, C being non empty binary-image of E holds (A (-) B) (-) C = A (-) (B (+) C)
let A, B, C be non empty binary-image of E; ::_thesis: (A (-) B) (-) C = A (-) (B (+) C)
 for x being set holds
( x in (A (-) B) (-) C iff x in A (-) (B (+) C) )
proof
let x be set ; ::_thesis: ( x in (A (-) B) (-) C iff x in A (-) (B (+) C) )
hereby  ::_thesis: ( x in A (-) (B (+) C) implies x in (A (-) B) (-) C )
assume  x in (A (-) B) (-) C ; ::_thesis: x in A (-) (B (+) C)
then consider w being Element of E such that
P1: ( x = w & ( for c being Element of E st c in C holds
w - c in A (-) B ) ) ;
now__::_thesis:_for_bc_being_Element_of_E_st_bc_in_B_(+)_C_holds_
w_-_bc_in_A
let bc be Element of E; ::_thesis: ( bc in B (+) C implies w - bc in A )
assume  bc in B (+) C ; ::_thesis: w - bc in A
then consider b, c being Element of E such that
P3: ( bc = b + c & b in B & c in C ) ;
 w - c in A (-) B by P1, P3;
then consider g being Element of E such that
P5: ( w - c = g & ( for b being Element of E st b in B holds
g - b in A ) ) ;
 w - bc = g - b by P3, RLVECT_1:27, P5;
hence  w - bc in A by P5, P3; ::_thesis: verum
end;
hence  x in A (-) (B (+) C) by P1; ::_thesis: verum
end;
assume  x in A (-) (B (+) C) ; ::_thesis: x in (A (-) B) (-) C
then consider w being Element of E such that
P1: ( x = w & ( for bc being Element of E st bc in B (+) C holds
w - bc in A ) ) ;
now__::_thesis:_for_c_being_Element_of_E_st_c_in_C_holds_
w_-_c_in_A_(-)_B
let c be Element of E; ::_thesis: ( c in C implies w - c in A (-) B )
assume P2: c in C ; ::_thesis: w - c in A (-) B
now__::_thesis:_for_b_being_Element_of_E_st_b_in_B_holds_
(w_-_c)_-_b_in_A
let b be Element of E; ::_thesis: ( b in B implies (w - c) - b in A )
assume P3: b in B ; ::_thesis: (w - c) - b in A
 b + c in B (+) C by P2, P3;
then  w - (b + c) in A by P1;
hence  (w - c) - b in A by RLVECT_1:27; ::_thesis: verum
end;
hence  w - c in A (-) B ; ::_thesis: verum
end;
hence  x in (A (-) B) (-) C by P1; ::_thesis: verum
end;
hence  (A (-) B) (-) C = A (-) (B (+) C) by TARSKI:1; ::_thesis: verum
end;

begin

definition
let E be RealLinearSpace;
let B be binary-image of E;
func dilation B ->  Function of (bool the carrier of E),(bool the carrier of E) means :def020: :: MORPH_01:def 2
 for A being binary-image of E holds it . A = A (+) B;
existence
 ex b1 being Function of (bool the carrier of E),(bool the carrier of E) st
for A being binary-image of E holds b1 . A = A (+) B
proof
defpred S1[ set , set ] means  ex A being binary-image of E st
( $1 = A & $2 = A (+) B );
X1: now__::_thesis:_for_x_being_set_st_x_in_bool_the_carrier_of_E_holds_
ex_y_being_set_st_
(_y_in_bool_the_carrier_of_E_&_S1[x,y]_)
let x be set ; ::_thesis: ( x in bool the carrier of E implies ex y being set st
( y in bool the carrier of E & S1[x,y] ) )
assume  x in bool the carrier of E ; ::_thesis: ex y being set st
( y in bool the carrier of E & S1[x,y] )
then reconsider A = x as binary-image of E ;
set y = A (+) B;
 A (+) B c= the carrier of E ;
hence  ex y being set st
( y in bool the carrier of E & S1[x,y] ) ; ::_thesis: verum
end;
consider f being Function of (bool the carrier of E),(bool the carrier of E) such that
X2: for x being set st x in bool the carrier of E holds
S1[x,f . x] from FUNCT_2:sch_1(X1);
take  f ; ::_thesis: for A being binary-image of E holds f . A = A (+) B
now__::_thesis:_for_A_being_binary-image_of_E_holds_f_._A_=_A_(+)_B
let A be binary-image of E; ::_thesis: f . A = A (+) B
 ex X being binary-image of E st
( A = X & f . A = X (+) B ) by X2;
hence  f . A = A (+) B ; ::_thesis: verum
end;
hence  for A being binary-image of E holds f . A = A (+) B ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (bool the carrier of E),(bool the carrier of E) st ( for A being binary-image of E holds b1 . A = A (+) B ) & ( for A being binary-image of E holds b2 . A = A (+) B ) holds
b1 = b2
proof
let f, g be Function of (bool the carrier of E),(bool the carrier of E); ::_thesis: ( ( for A being binary-image of E holds f . A = A (+) B ) & ( for A being binary-image of E holds g . A = A (+) B ) implies f = g )
assume A1: for A being binary-image of E holds f . A = A (+) B ; ::_thesis: ( ex A being binary-image of E st not g . A = A (+) B or f = g )
assume A2: for A being binary-image of E holds g . A = A (+) B ; ::_thesis: f = g
now__::_thesis:_for_x_being_set_st_x_in_bool_the_carrier_of_E_holds_
f_._x_=_g_._x
let x be set ; ::_thesis: ( x in bool the carrier of E implies f . x = g . x )
assume  x in bool the carrier of E ; ::_thesis: f . x = g . x
then reconsider A = x as binary-image of E ;
thus f . x = A (+) B by A1
.= g . x by A2 ; ::_thesis: verum
end;
hence  f = g by FUNCT_2:12; ::_thesis: verum
end;
end;

:: deftheorem def020 defines dilation MORPH_01:def_2_:_
 for E being RealLinearSpace
for B being binary-image of E
for b3 being Function of (bool the carrier of E),(bool the carrier of E) holds
( b3 = dilation B iff for A being binary-image of E holds b3 . A = A (+) B );

definition
let E be RealLinearSpace;
let B be binary-image of E;
func erosion B ->  Function of (bool the carrier of E),(bool the carrier of E) means :def030: :: MORPH_01:def 3
 for A being binary-image of E holds it . A = A (-) B;
existence
 ex b1 being Function of (bool the carrier of E),(bool the carrier of E) st
for A being binary-image of E holds b1 . A = A (-) B
proof
defpred S1[ set , set ] means  ex A being binary-image of E st
( $1 = A & $2 = A (-) B );
X1: now__::_thesis:_for_x_being_set_st_x_in_bool_the_carrier_of_E_holds_
ex_y_being_set_st_
(_y_in_bool_the_carrier_of_E_&_S1[x,y]_)
let x be set ; ::_thesis: ( x in bool the carrier of E implies ex y being set st
( y in bool the carrier of E & S1[x,y] ) )
assume  x in bool the carrier of E ; ::_thesis: ex y being set st
( y in bool the carrier of E & S1[x,y] )
then reconsider A = x as binary-image of E ;
set y = A (-) B;
 A (-) B c= the carrier of E ;
hence  ex y being set st
( y in bool the carrier of E & S1[x,y] ) ; ::_thesis: verum
end;
consider f being Function of (bool the carrier of E),(bool the carrier of E) such that
X2: for x being set st x in bool the carrier of E holds
S1[x,f . x] from FUNCT_2:sch_1(X1);
take  f ; ::_thesis: for A being binary-image of E holds f . A = A (-) B
now__::_thesis:_for_A_being_binary-image_of_E_holds_f_._A_=_A_(-)_B
let A be binary-image of E; ::_thesis: f . A = A (-) B
 ex X being binary-image of E st
( A = X & f . A = X (-) B ) by X2;
hence  f . A = A (-) B ; ::_thesis: verum
end;
hence  for A being binary-image of E holds f . A = A (-) B ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of (bool the carrier of E),(bool the carrier of E) st ( for A being binary-image of E holds b1 . A = A (-) B ) & ( for A being binary-image of E holds b2 . A = A (-) B ) holds
b1 = b2
proof
let f, g be Function of (bool the carrier of E),(bool the carrier of E); ::_thesis: ( ( for A being binary-image of E holds f . A = A (-) B ) & ( for A being binary-image of E holds g . A = A (-) B ) implies f = g )
assume that
A1: for A being binary-image of E holds f . A = A (-) B and
A2: for A being binary-image of E holds g . A = A (-) B ; ::_thesis: f = g
now__::_thesis:_for_x_being_set_st_x_in_bool_the_carrier_of_E_holds_
f_._x_=_g_._x
let x be set ; ::_thesis: ( x in bool the carrier of E implies f . x = g . x )
assume  x in bool the carrier of E ; ::_thesis: f . x = g . x
then reconsider A = x as binary-image of E ;
thus f . x = A (-) B by A1
.= g . x by A2 ; ::_thesis: verum
end;
hence  f = g by FUNCT_2:12; ::_thesis: verum
end;
end;

:: deftheorem def030 defines erosion MORPH_01:def_3_:_
 for E being RealLinearSpace
for B being binary-image of E
for b3 being Function of (bool the carrier of E),(bool the carrier of E) holds
( b3 = erosion B iff for A being binary-image of E holds b3 . A = A (-) B );

theorem :: MORPH_01:26
for E being RealLinearSpace
for F being binary-image-family of E
for B being non empty binary-image of E holds (dilation B) . (union F) = union  {  ((dilation B) . X) where X is binary-image of E : X in F  }
proof
let E be RealLinearSpace; ::_thesis: for F being binary-image-family of E
for B being non empty binary-image of E holds (dilation B) . (union F) = union  {  ((dilation B) . X) where X is binary-image of E : X in F  }
let F be binary-image-family of E; ::_thesis: for B being non empty binary-image of E holds (dilation B) . (union F) = union  {  ((dilation B) . X) where X is binary-image of E : X in F  }
let B be non empty binary-image of E; ::_thesis: (dilation B) . (union F) = union  {  ((dilation B) . X) where X is binary-image of E : X in F  }
P2: for x being set holds
( x in  {  (X (+) B) where X is binary-image of E : X in F  }  iff x in  {  ((dilation B) . X) where X is binary-image of E : X in F  }  )
proof
let x be set ; ::_thesis: ( x in  {  (X (+) B) where X is binary-image of E : X in F  }  iff x in  {  ((dilation B) . X) where X is binary-image of E : X in F  }  )
hereby  ::_thesis: ( x in  {  ((dilation B) . X) where X is binary-image of E : X in F  }  implies x in  {  (X (+) B) where X is binary-image of E : X in F  }  )
assume  x in  {  (X (+) B) where X is binary-image of E : X in F  }  ; ::_thesis: x in  {  ((dilation B) . W) where W is binary-image of E : W in F  }
then consider X being binary-image of E such that
P3: ( x = X (+) B & X in F ) ;
 ( x = (dilation B) . X & X in F ) by P3, def020;
hence  x in  {  ((dilation B) . W) where W is binary-image of E : W in F  }  ; ::_thesis: verum
end;
assume  x in  {  ((dilation B) . X) where X is binary-image of E : X in F  }  ; ::_thesis: x in  {  (X (+) B) where X is binary-image of E : X in F  }
then consider X being binary-image of E such that
P3: ( x = (dilation B) . X & X in F ) ;
 ( x = X (+) B & X in F ) by P3, def020;
hence  x in  {  (W (+) B) where W is binary-image of E : W in F  }  ; ::_thesis: verum
end;
thus (dilation B) . (union F) = (union F) (+) B by def020
.= union  {  (X (+) B) where X is binary-image of E : X in F  }  by Th108B
.= union  {  ((dilation B) . X) where X is binary-image of E : X in F  }  by P2, TARSKI:1 ; ::_thesis: verum
end;

theorem :: MORPH_01:27
for E being RealLinearSpace
for A, B, C being non empty binary-image of E st A c= B holds
(dilation C) . A c= (dilation C) . B
proof
let E be RealLinearSpace; ::_thesis: for A, B, C being non empty binary-image of E st A c= B holds
(dilation C) . A c= (dilation C) . B
let A, B, C be non empty binary-image of E; ::_thesis: ( A c= B implies (dilation C) . A c= (dilation C) . B )
assume AS: A c= B ; ::_thesis: (dilation C) . A c= (dilation C) . B
P1: (dilation C) . A = C + A by def020;
 (dilation C) . B = C + B by def020;
hence  (dilation C) . A c= (dilation C) . B by P1, AS, Th112; ::_thesis: verum
end;

theorem :: MORPH_01:28
for E being RealLinearSpace
for v being Element of E
for C, A being non empty binary-image of E holds (dilation C) . (v + A) = v + ((dilation C) . A)
proof
let E be RealLinearSpace; ::_thesis: for v being Element of E
for C, A being non empty binary-image of E holds (dilation C) . (v + A) = v + ((dilation C) . A)
let v be Element of E; ::_thesis: for C, A being non empty binary-image of E holds (dilation C) . (v + A) = v + ((dilation C) . A)
let C, A be non empty binary-image of E; ::_thesis: (dilation C) . (v + A) = v + ((dilation C) . A)
P1: (dilation C) . (v + A) = (v + A) (+) C by def020;
 v + ((dilation C) . A) = v + (A (+) C) by def020;
hence  (dilation C) . (v + A) = v + ((dilation C) . A) by Th113, P1; ::_thesis: verum
end;

theorem :: MORPH_01:29
for E being RealLinearSpace
for F being binary-image-family of E
for B being non empty binary-image of E holds (erosion B) . (meet F) = meet  {  ((erosion B) . X) where X is binary-image of E : X in F  }
proof
let E be RealLinearSpace; ::_thesis: for F being binary-image-family of E
for B being non empty binary-image of E holds (erosion B) . (meet F) = meet  {  ((erosion B) . X) where X is binary-image of E : X in F  }
let F be binary-image-family of E; ::_thesis: for B being non empty binary-image of E holds (erosion B) . (meet F) = meet  {  ((erosion B) . X) where X is binary-image of E : X in F  }
let B be non empty binary-image of E; ::_thesis: (erosion B) . (meet F) = meet  {  ((erosion B) . X) where X is binary-image of E : X in F  }
P2: for x being set holds
( x in  {  (X (-) B) where X is binary-image of E : X in F  }  iff x in  {  ((erosion B) . X) where X is binary-image of E : X in F  }  )
proof
let x be set ; ::_thesis: ( x in  {  (X (-) B) where X is binary-image of E : X in F  }  iff x in  {  ((erosion B) . X) where X is binary-image of E : X in F  }  )
hereby  ::_thesis: ( x in  {  ((erosion B) . X) where X is binary-image of E : X in F  }  implies x in  {  (X (-) B) where X is binary-image of E : X in F  }  )
assume  x in  {  (X (-) B) where X is binary-image of E : X in F  }  ; ::_thesis: x in  {  ((erosion B) . W) where W is binary-image of E : W in F  }
then consider X being binary-image of E such that
P3: ( x = X (-) B & X in F ) ;
 ( x = (erosion B) . X & X in F ) by P3, def030;
hence  x in  {  ((erosion B) . W) where W is binary-image of E : W in F  }  ; ::_thesis: verum
end;
assume  x in  {  ((erosion B) . X) where X is binary-image of E : X in F  }  ; ::_thesis: x in  {  (X (-) B) where X is binary-image of E : X in F  }
then consider X being binary-image of E such that
P3: ( x = (erosion B) . X & X in F ) ;
 ( x = X (-) B & X in F ) by P3, def030;
hence  x in  {  (W (-) B) where W is binary-image of E : W in F  }  ; ::_thesis: verum
end;
thus (erosion B) . (meet F) = (meet F) (-) B by def030
.= meet  {  (X (-) B) where X is binary-image of E : X in F  }  by Th114
.= meet  {  ((erosion B) . X) where X is binary-image of E : X in F  }  by P2, TARSKI:1 ; ::_thesis: verum
end;

theorem :: MORPH_01:30
for E being RealLinearSpace
for A, B, C being non empty binary-image of E st A c= B holds
(erosion C) . A c= (erosion C) . B
proof
let E be RealLinearSpace; ::_thesis: for A, B, C being non empty binary-image of E st A c= B holds
(erosion C) . A c= (erosion C) . B
let A, B, C be non empty binary-image of E; ::_thesis: ( A c= B implies (erosion C) . A c= (erosion C) . B )
assume AS: A c= B ; ::_thesis: (erosion C) . A c= (erosion C) . B
P1: (erosion C) . A = A (-) C by def030;
 (erosion C) . B = B (-) C by def030;
hence  (erosion C) . A c= (erosion C) . B by P1, AS, Th118; ::_thesis: verum
end;

theorem :: MORPH_01:31
for E being RealLinearSpace
for v being Element of E
for C, A being non empty binary-image of E holds (erosion C) . (v + A) = v + ((erosion C) . A)
proof
let E be RealLinearSpace; ::_thesis: for v being Element of E
for C, A being non empty binary-image of E holds (erosion C) . (v + A) = v + ((erosion C) . A)
let v be Element of E; ::_thesis: for C, A being non empty binary-image of E holds (erosion C) . (v + A) = v + ((erosion C) . A)
let C, A be non empty binary-image of E; ::_thesis: (erosion C) . (v + A) = v + ((erosion C) . A)
P1: (erosion C) . (v + A) = (v + A) (-) C by def030;
 v + ((erosion C) . A) = v + (A (-) C) by def030;
hence  (erosion C) . (v + A) = v + ((erosion C) . A) by Th120, P1; ::_thesis: verum
end;

theorem :: MORPH_01:32
for E being RealLinearSpace
for C, A being non empty binary-image of E holds
( (dilation C) . ( the carrier of E \ A) = the carrier of E \ ((erosion C) . A) & (erosion C) . ( the carrier of E \ A) = the carrier of E \ ((dilation C) . A) )
proof
let E be RealLinearSpace; ::_thesis: for C, A being non empty binary-image of E holds
( (dilation C) . ( the carrier of E \ A) = the carrier of E \ ((erosion C) . A) & (erosion C) . ( the carrier of E \ A) = the carrier of E \ ((dilation C) . A) )
let C, A be non empty binary-image of E; ::_thesis: ( (dilation C) . ( the carrier of E \ A) = the carrier of E \ ((erosion C) . A) & (erosion C) . ( the carrier of E \ A) = the carrier of E \ ((dilation C) . A) )
thus (dilation C) . ( the carrier of E \ A) = ( the carrier of E \ A) (+) C by def020
.= the carrier of E \ (A (-) C) by Th106
.= the carrier of E \ ((erosion C) . A) by def030 ; ::_thesis: (erosion C) . ( the carrier of E \ A) = the carrier of E \ ((dilation C) . A)
thus (erosion C) . ( the carrier of E \ A) = ( the carrier of E \ A) (-) C by def030
.= the carrier of E \ (A (+) C) by Th106
.= the carrier of E \ ((dilation C) . A) by def020 ; ::_thesis: verum
end;

theorem :: MORPH_01:33
for E being RealLinearSpace
for C, B, A being non empty binary-image of E holds
( (dilation C) . ((dilation B) . A) = (dilation ((dilation C) . B)) . A & (erosion C) . ((erosion B) . A) = (erosion ((dilation C) . B)) . A )
proof
let E be RealLinearSpace; ::_thesis: for C, B, A being non empty binary-image of E holds
( (dilation C) . ((dilation B) . A) = (dilation ((dilation C) . B)) . A & (erosion C) . ((erosion B) . A) = (erosion ((dilation C) . B)) . A )
let C, B, A be non empty binary-image of E; ::_thesis: ( (dilation C) . ((dilation B) . A) = (dilation ((dilation C) . B)) . A & (erosion C) . ((erosion B) . A) = (erosion ((dilation C) . B)) . A )
thus (dilation C) . ((dilation B) . A) = (dilation C) . (A (+) B) by def020
.= (A (+) B) (+) C by def020
.= A (+) (B (+) C) by Th108A1
.= A (+) ((dilation C) . B) by def020
.= (dilation ((dilation C) . B)) . A by def020 ; ::_thesis: (erosion C) . ((erosion B) . A) = (erosion ((dilation C) . B)) . A
thus (erosion C) . ((erosion B) . A) = (erosion C) . (A (-) B) by def030
.= (A (-) B) (-) C by def030
.= A (-) (B (+) C) by Th121
.= A (-) ((dilation C) . B) by def020
.= (erosion ((dilation C) . B)) . A by def030 ; ::_thesis: verum
end;