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

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

hence
F = G
; :: thesis: verumlet 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;thus F . f = (Q * f) * (P ") by A3

.= G . f by A4 ; :: thesis: verum