defpred S1[ 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 S1[f,g,y]
proof
let f be
Element of
PFuncs (
A,
B);
for g being Element of PFuncs (B,C) ex y being Element of PFuncs (A,C) st S1[f,g,y]let g be
Element of
PFuncs (
B,
C);
ex y being Element of PFuncs (A,C) st S1[f,g,y]
reconsider h =
g * f as
Element of
PFuncs (
A,
C)
by PARTFUN1:45;
take
h
;
S1[f,g,h]
thus
S1[
f,
g,
h]
;
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 S1[x,y,F . (x,y)]
from BINOP_1:sch 3(A1);
take
F
; 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; for g being PartFunc of B,C holds F . (f,g) = g * f
let g be PartFunc of B,C; 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; verum