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