let F, G be Function of [:(PFuncs (A,B)),(PFuncs (B,C)):],(PFuncs (A,C)); ( ( for f being PartFunc of A,B
for g being PartFunc of B,C holds F . (f,g) = g * f ) & ( for f being PartFunc of A,B
for g being PartFunc of B,C holds G . (f,g) = g * f ) implies F = G )
assume that
A3:
for f being PartFunc of A,B
for g being PartFunc of B,C holds F . (f,g) = g * f
and
A4:
for f being PartFunc of A,B
for g being PartFunc of B,C holds G . (f,g) = g * f
; F = G
let x, y be set ; BINOP_1:def 21 ( not x in PFuncs (A,B) or not y in PFuncs (B,C) or F . (x,y) = G . (x,y) )
assume
x in PFuncs (A,B)
; ( not y in PFuncs (B,C) or F . (x,y) = G . (x,y) )
then reconsider f = x as PartFunc of A,B by PARTFUN1:46;
assume
y in PFuncs (B,C)
; F . (x,y) = G . (x,y)
then reconsider g = y as PartFunc of B,C by PARTFUN1:46;
thus F . (x,y) =
g * f
by A3
.=
G . (x,y)
by A4
; verum