let F, G be Cardinal-Function; :: thesis: ( F c= G & not 0 in rng G implies Product F c= Product G )
assume A1: F c= G ; :: thesis: ( 0 in rng G or Product F c= Product G )
then A2: ( dom F c= dom G & ( for x being set st x in dom F holds
F . x = G . x ) ) by GRFUNC_1:8;
assume A3: not 0 in rng G ; :: thesis: Product F c= Product G
deffunc H₁( Function) -> set = $1 | (dom F);
consider f being Function such that
A4: ( dom f = product G & ( for g being Function st g in product G holds
f . g = H₁(g) ) ) from FUNCT_5:sch 1();
product F c= rng f

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in product F or x in rng f )
assume x in product F ; :: thesis: x in rng f
then consider g being Function such that
A5: ( x = g & dom g = dom F & ( for x being set st x in dom F holds
g . x in F . x ) ) by Def5;
A6: product G <> {} by A3, Th37;
consider y being Element of product G;
consider h being Function such that
A7: ( y = h & dom h = dom G & ( for x being set st x in dom G holds
h . x in G . x ) ) by A6, Def5;
deffunc H₂( set ) -> set = g . $1;
deffunc H₃( set ) -> set = h . $1;
defpred S₂[ set ] means $1 in dom F;
consider f1 being Function such that
A8: ( dom f1 = dom G & ( for x being set st x in dom G holds
( ( S₂[x] implies f1 . x = H₂(x) ) & ( not S₂[x] implies f1 . x = H₃(x) ) ) ) ) from PARTFUN1:sch 1();

now

let z be set ; :: thesis: ( z in dom G implies f1 . z in G . z )
assume A9: z in dom G ; :: thesis: f1 . z in G . z

A10: now

assume z in dom F ; :: thesis: f1 . z in G . z
then ( f1 . z = g . z & g . z in F . z & F . z = G . z ) by A1, A5, A8, A9, GRFUNC_1:8;
hence f1 . z in G . z ; :: thesis: verum

end;

( ( not z in dom F implies f1 . z = h . z ) & h . z in G . z ) by A7, A8, A9;
hence f1 . z in G . z by A10; :: thesis: verum

end;

then A11: f1 in product G by A8, Def5;
then A12: ( f . f1 = f1 | (dom F) & dom (f1 | (dom F)) = dom F ) by A2, A4, A8, RELAT_1:91;

now

let z be set ; :: thesis: ( z in dom F implies (f1 | (dom F)) . z = g . z )
assume z in dom F ; :: thesis: (f1 | (dom F)) . z = g . z
then ( (f1 | (dom F)) . z = f1 . z & z in dom G & ( z in dom G implies f1 . z = g . z ) ) by A2, A8, A12, FUNCT_1:70;
hence (f1 | (dom F)) . z = g . z ; :: thesis: verum

end;

then f . f1 = g by A5, A12, FUNCT_1:9;
hence x in rng f by A4, A5, A11, FUNCT_1:def 5; :: thesis: verum

end;

hence Product F c= Product G by A4, CARD_1:28; :: thesis: verum