defpred S₁[ object , object ] means ex A being binary-image of E st
( $1 = A & $2 = A (-) B );

let x be object ; :: thesis:
assume x in bool the carrier of E ; :: thesis:
then reconsider A = x as binary-image of E ;
set y = A (-) B;
A (-) B c= the carrier of E ;
hence ex y being object st
( y in bool the carrier of E & S₁[x,y] ) ; :: thesis:

end;

consider f being Function of (bool the carrier of E),(bool the carrier of E) such that
A2: for x being object st x in bool the carrier of E holds
S₁[x,f . x] from FUNCT_2:sch 1(A1);
take f ; :: thesis:

end;