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

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 by FUNCT_2:113; :: thesis: verum