defpred S₁[ 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₁[f,g,y]

proof

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₁[f,g,y]
let g be Element of PFuncs (B,C); :: thesis: ex y being Element of PFuncs (A,C) st S₁[f,g,y]
reconsider h = g * f as Element of PFuncs (A,C) by PARTFUN1:45;
take h ; :: thesis: S₁[f,g,h]
thus S₁[f,g,h] ; :: thesis: verum

end;

consider F being Function of [:(PFuncs (A,B)),(PFuncs (B,C)):],(PFuncs (A,C)) such that
A2: for x being Element of PFuncs (A,B)
for y being Element of PFuncs (B,C) holds S₁[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