let F1, F2 be Function of [: the carrier of R, the carrier of M:], the carrier of M; :: 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 & F1 . (x,y) = h . y ) ) & ( 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 & F2 . (x,y) = h . y ) ) implies F1 = F2 )
assume that
A4: 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 & F1 . (x,y) = h . y ) and
A5: 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 & F2 . (x,y) = h . y ) ; :: thesis: F1 = F2

now :: thesis: for x being Element of the carrier of R
for y being Element of the carrier of M holds F1 . (x,y) = F2 . (x,y)

let x be Element of the carrier of R; :: thesis: for y being Element of the carrier of M holds F1 . (x,y) = F2 . (x,y)
let y be Element of the carrier of M; :: thesis: F1 . (x,y) = F2 . (x,y)
consider h1 being Endomorphism of M such that
A6: ( h1 = s . x & F1 . (x,y) = h1 . y ) by A4;
consider h2 being Endomorphism of M such that
A7: ( h2 = s . x & F2 . (x,y) = h2 . y ) by A5;
thus F1 . (x,y) = F2 . (x,y) by A6, A7; :: thesis: verum

end;

hence F1 = F2 ; :: thesis: verum