defpred S₁[ object , object ] means ( ( not $1 in K & $2 = $1 ) or ( $1 in K & $2 = f . $1 ) );
M: for x being object st x in [#] (embField f) holds
ex y being object st
( y in [#] F & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in [#] (embField f) implies ex y being object st
( y in [#] F & S₁[x,y] ) )
assume M0: x in [#] (embField f) ; :: thesis: ex y being object st
( y in [#] F & S₁[x,y] )
then reconsider x1 = x as Element of (embField f) ;

per cases ( x in K or not x in K ) ;

suppose M1: x in K ; :: thesis: ex y being object st
( y in [#] F & S₁[x,y] )

then reconsider a = x as Element of K ;
take b = f . a; :: thesis: ( b in [#] F & S₁[x,b] )
thus b in [#] F ; :: thesis: S₁[x,b]
thus S₁[x,b] by M1; :: thesis: verum

end;

suppose M1: not x in K ; :: thesis: ex y being object st
( y in [#] F & S₁[x,y] )

take x ; :: thesis: ( x in [#] F & S₁[x,x] )
reconsider x1 = x as Element of carr f by M0, defemb;
( x1 in [#] F & not x1 in rng f ) by M1, Lm1;
hence x in [#] F ; :: thesis: S₁[x,x]
thus S₁[x,x] by M1; :: thesis: verum

end;

end;

end;

consider g being Function of ([#] (embField f)),([#] F) such that
N: for x being object st x in [#] (embField f) holds
S₁[x,g . x] from FUNCT_2:sch 1(M);
reconsider g = g as Function of (embField f),F ;
take g ; :: thesis: ( ( for a being Element of (embField f) st not a in K holds
g . a = a ) & ( for a being Element of (embField f) st a in K holds
g . a = f . a ) )
thus ( ( for a being Element of (embField f) st not a in K holds
g . a = a ) & ( for a being Element of (embField f) st a in K holds
g . a = f . a ) ) by N; :: thesis: verum