defpred S1[ object , object ] means ex g, h being Function st
( $1 = g & $2 = h & dom h = dom f & ( for z being object st z in dom h holds
h . z = (uncurry f) . (z,(g . z)) ) );
A1:
for x being object st x in product (doms f) holds
ex y being object st S1[x,y]
consider F being Function such that
A4:
( dom F = product (doms f) & ( for x being object st x in product (doms f) holds
S1[x,F . x] ) )
from CLASSES1:sch 1(A1);
take
F
; ( dom F = product (doms f) & ( for g being Function st g in product (doms f) holds
ex h being Function st
( F . g = h & dom h = dom f & ( for x being object st x in dom h holds
h . x = (uncurry f) . (x,(g . x)) ) ) ) )
thus
dom F = product (doms f)
by A4; for g being Function st g in product (doms f) holds
ex h being Function st
( F . g = h & dom h = dom f & ( for x being object st x in dom h holds
h . x = (uncurry f) . (x,(g . x)) ) )
let g be Function; ( g in product (doms f) implies ex h being Function st
( F . g = h & dom h = dom f & ( for x being object st x in dom h holds
h . x = (uncurry f) . (x,(g . x)) ) ) )
assume
g in product (doms f)
; ex h being Function st
( F . g = h & dom h = dom f & ( for x being object st x in dom h holds
h . x = (uncurry f) . (x,(g . x)) ) )
then
ex g1, h being Function st
( g = g1 & F . g = h & dom h = dom f & ( for z being object st z in dom h holds
h . z = (uncurry f) . (z,(g1 . z)) ) )
by A4;
hence
ex h being Function st
( F . g = h & dom h = dom f & ( for x being object st x in dom h holds
h . x = (uncurry f) . (x,(g . x)) ) )
; verum