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

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