let F, G be Function of [:(PFuncs (A,B)),(PFuncs (B,C)):],(PFuncs (A,C)); :: thesis: ( ( 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 ; :: thesis: F = G
let x, y be set ; :: according to BINOP_1:def 21 :: thesis: ( 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) ; :: thesis: ( 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) ; :: thesis: 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 ; :: thesis: verum