defpred S1[ object , object , object ] means $1 = F4($3,$2);
A2:
for i being object st i in F1() holds
for x being object st x in F2() . i holds
ex y being object st
( y in F3() . i & S1[y,x,i] )
by A1;
consider F being ManySortedFunction of F2(),F3() such that
A3:
for i being object st i in F1() holds
ex f being Function of (F2() . i),(F3() . i) st
( f = F . i & ( for x being object st x in F2() . i holds
S1[f . x,x,i] ) )
from MSSUBFAM:sch 1(A2);
take
F
; for i being Element of F1()
for a being Element of F2() . i holds (F . i) . a = F4(i,a)
let i be Element of F1(); for a being Element of F2() . i holds (F . i) . a = F4(i,a)
let a be Element of F2() . i; (F . i) . a = F4(i,a)
consider f being Function of (F2() . i),(F3() . i) such that
A4:
( f = F . i & ( for x being object st x in F2() . i holds
S1[f . x,x,i] ) )
by A3;
thus
(F . i) . a = F4(i,a)
by A4; verum