defpred S₁[ Element of the carrier of R, Element of the carrier of M, Element of the carrier of M] means ex h being additive Function of the carrier of M, the carrier of M st
( h = s . $1 & $3 = h . $2 );
A1: for x being Element of the carrier of R
for y being Element of the carrier of M ex z being Element of the carrier of M st S₁[x,y,z]

proof

let x be Element of the carrier of R; :: thesis: for y being Element of the carrier of M ex z being Element of the carrier of M st S₁[x,y,z]
let y be Element of the carrier of M; :: thesis: ex z being Element of the carrier of M st S₁[x,y,z]
s . x in set_End M ;
then consider h being Function of the carrier of M, the carrier of M such that
A2: ( h = s . x & h is Endomorphism of M ) ;
reconsider z = h . y as Element of the carrier of M ;
take z ; :: thesis: S₁[x,y,z]
thus S₁[x,y,z] by A2; :: thesis: verum

end;

consider f being Function of [: the carrier of R, the carrier of M:], the carrier of M such that
A3: for x being Element of the carrier of R
for y being Element of the carrier of M holds S₁[x,y,f . (x,y)] from BINOP_1:sch 3(A1);
take f ; :: thesis: for x being Element of the carrier of R
for y being Element of the carrier of M ex h being Endomorphism of M st
( h = s . x & f . (x,y) = h . y )
let x be Element of the carrier of R; :: thesis: for y being Element of the carrier of M ex h being Endomorphism of M st
( h = s . x & f . (x,y) = h . y )
let y be Element of the carrier of M; :: thesis: ex h being Endomorphism of M st
( h = s . x & f . (x,y) = h . y )
thus ex h being Endomorphism of M st
( h = s . x & f . (x,y) = h . y ) by A3; :: thesis: verum