let F, G be Function of (Funcs (A,B)),(Funcs (A,B)); :: thesis: ( ( for f being Function of A,B holds F . f = (Q * f) * (P ") ) & ( for f being Function of A,B holds G . f = (Q * f) * (P ") ) implies F = G )
assume that
A3: for f being Function of A,B holds F . f = (Q * f) * (P ") and
A4: for f being Function of A,B holds G . f = (Q * f) * (P ") ; :: thesis: F = G

now :: thesis: for f being Element of Funcs (A,B) holds F . f = G . f

let f be Element of Funcs (A,B); :: thesis: F . f = G . f
thus F . f = (Q * f) * (P ") by A3
.= G . f by A4 ; :: thesis: verum

end;

hence F = G ; :: thesis: verum