defpred S₂[ object ] means ex g being Function st
( f = g & dom g c= dom f & ( for x being object st x in dom g holds
g . x in f . x ) );
consider A being set such that
A1: for x being object holds
( x in A iff ( x in PFuncs ((dom f),(union (rng f))) & S₂[x] ) ) from XBOOLE_0:sch 1();
{} is PartFunc of (dom f),(union (rng f)) by RELSET_1:12;
then A2: {} in PFuncs ((dom f),(union (rng f))) by PARTFUN1:45;
A3: dom {} c= dom f ;
A4: for x being object st x in dom {} holds
{} . x in f . x ;

now :: thesis: for x being object st x in A holds
x is Function

let x be object ; :: thesis: ( x in A implies x is Function )
assume x in A ; :: thesis: x is Function
then ex g being Function st
( x = g & dom g c= dom f & ( for x being object st x in dom g holds
g . x in f . x ) ) by A1;
hence x is Function ; :: thesis: verum

end;

then reconsider A = A as non empty functional set by A1, A2, A3, A4, FUNCT_1:def 13;

now :: thesis: for x being object holds
( ( x in A implies ex g being Function st
( x = g & dom g c= dom f & ( for x being object st x in dom g holds
g . x in f . x ) ) ) & ( ex g being Function st
( x = g & dom g c= dom f & ( for x being object st x in dom g holds
g . x in f . x ) ) implies x in A ) )

let x be object ; :: thesis: ( ( x in A implies ex g being Function st
( x = g & dom g c= dom f & ( for x being object st x in dom g holds
g . x in f . x ) ) ) & ( ex g being Function st
( x = g & dom g c= dom f & ( for x being object st x in dom g holds
g . x in f . x ) ) implies x in A ) )
thus ( x in A implies ex g being Function st
( x = g & dom g c= dom f & ( for x being object st x in dom g holds
g . x in f . x ) ) ) by A1; :: thesis: ( ex g being Function st
( x = g & dom g c= dom f & ( for x being object st x in dom g holds
g . x in f . x ) ) implies x in A )
given g being Function such that A5: x = g and
A6: dom g c= dom f and
A7: for x being object st x in dom g holds
g . x in f . x ; :: thesis: x in A
rng g c= union (rng f)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng g or y in union (rng f) )
assume y in rng g ; :: thesis: y in union (rng f)
then consider z being object such that
A8: z in dom g and
A9: y = g . z by FUNCT_1:def 3;
A10: g . z in f . z by A7, A8;
f . z in rng f by A6, A8, FUNCT_1:def 3;
hence y in union (rng f) by A9, A10, TARSKI:def 4; :: thesis: verum

end;

then x in PFuncs ((dom f),(union (rng f))) by A5, A6, PARTFUN1:def 3;
hence x in A by A1, A5, A6, A7; :: thesis: verum

end;

hence ( sproduct f is functional & not sproduct f is empty ) by Def9; :: thesis: verum