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] )

let x be object ; :: thesis:
assume M0: x in [#] (embField f) ; :: thesis:
then reconsider x1 = x as Element of (embField f) ;

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

end;

take x ; :: thesis:
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:
thus S₁[x,x] by M1; :: thesis:

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:
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: