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

proof

let x be object ; :: thesis: ( x in product (doms f) implies ex y being object st S₁[x,y] )
assume x in product (doms f) ; :: thesis: ex y being object st S₁[x,y]
then consider g being Function such that
A2: x = g and
dom g = dom (doms f) and
for x being object st x in dom (doms f) holds
g . x in (doms f) . x by CARD_3:def 5;
deffunc H₁( object ) -> set = (uncurry f) . [$1,(g . $1)];
consider h being Function such that
A3: ( dom h = dom f & ( for z being object st z in dom f holds
h . z = H₁(z) ) ) from FUNCT_1:sch 3();
reconsider y = h as set ;
take y ; :: thesis: S₁[x,y]
take g ; :: thesis: ex h being Function st
( x = g & y = h & dom h = dom f & ( for z being object st z in dom h holds
h . z = (uncurry f) . (z,(g . z)) ) )
take h ; :: thesis: ( x = g & y = h & dom h = dom f & ( for z being object st z in dom h holds
h . z = (uncurry f) . (z,(g . z)) ) )
thus ( x = g & y = h & dom h = dom f & ( for z being object st z in dom h holds
h . z = (uncurry f) . (z,(g . z)) ) ) by A2, A3; :: thesis: verum

end;

consider F being Function such that
A4: ( dom F = product (doms f) & ( for x being object st x in product (doms f) holds
S₁[x,F . x] ) ) from CLASSES1:sch 1(A1);
take F ; :: thesis: ( 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; :: thesis: 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; :: thesis: ( 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) ; :: thesis: 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)) ) ) ; :: thesis: verum