defpred S_{1}[ Function, Function, object ] means $3 = $2 * $1;

A1: for f being Element of PFuncs (A,B)

for g being Element of PFuncs (B,C) ex y being Element of PFuncs (A,C) st S_{1}[f,g,y]

A2: for x being Element of PFuncs (A,B)

for y being Element of PFuncs (B,C) holds S_{1}[x,y,F . (x,y)]
from BINOP_1:sch 3(A1);

take F ; :: thesis: for f being PartFunc of A,B

for g being PartFunc of B,C holds F . (f,g) = g * f

let f be PartFunc of A,B; :: thesis: for g being PartFunc of B,C holds F . (f,g) = g * f

let g be PartFunc of B,C; :: thesis: F . (f,g) = g * f

( f in PFuncs (A,B) & g in PFuncs (B,C) ) by PARTFUN1:45;

hence F . (f,g) = g * f by A2; :: thesis: verum

A1: for f being Element of PFuncs (A,B)

for g being Element of PFuncs (B,C) ex y being Element of PFuncs (A,C) st S

proof

consider F being Function of [:(PFuncs (A,B)),(PFuncs (B,C)):],(PFuncs (A,C)) such that
let f be Element of PFuncs (A,B); :: thesis: for g being Element of PFuncs (B,C) ex y being Element of PFuncs (A,C) st S_{1}[f,g,y]

let g be Element of PFuncs (B,C); :: thesis: ex y being Element of PFuncs (A,C) st S_{1}[f,g,y]

reconsider h = g * f as Element of PFuncs (A,C) by PARTFUN1:45;

take h ; :: thesis: S_{1}[f,g,h]

thus S_{1}[f,g,h]
; :: thesis: verum

end;let g be Element of PFuncs (B,C); :: thesis: ex y being Element of PFuncs (A,C) st S

reconsider h = g * f as Element of PFuncs (A,C) by PARTFUN1:45;

take h ; :: thesis: S

thus S

A2: for x being Element of PFuncs (A,B)

for y being Element of PFuncs (B,C) holds S

take F ; :: thesis: for f being PartFunc of A,B

for g being PartFunc of B,C holds F . (f,g) = g * f

let f be PartFunc of A,B; :: thesis: for g being PartFunc of B,C holds F . (f,g) = g * f

let g be PartFunc of B,C; :: thesis: F . (f,g) = g * f

( f in PFuncs (A,B) & g in PFuncs (B,C) ) by PARTFUN1:45;

hence F . (f,g) = g * f by A2; :: thesis: verum