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 by GRFUNC_1:2;
assume A3: not 0 in rng G ; :: thesis: Product F c= Product G
deffunc H1( 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 = H1(g) ) ) from FUNCT_5:sch 1();
 product F c= rng f
proof
let x be object ; :: 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 and
A6: dom g = dom F and
A7: for x being object st x in dom F holds
g . x in F . x by Def5;
A8: product G <> {} by A3, Th26;
set y = the Element of product G;
consider h being Function such that
the Element of product G = h and
dom h = dom G and
A9: for x being object st x in dom G holds
h . x in G . x by A8, Def5;
deffunc H2( object ) -> set = g . $1;
deffunc H3( object ) -> set = h . $1;
defpred S2[ object ] means $1 in dom F;
consider f1 being Function such that
A10: ( dom f1 = dom G & ( for x being object st x in dom G holds
( ( S2[x] implies f1 . x = H2(x) ) & ( not S2[x] implies f1 . x = H3(x) ) ) ) ) from PARTFUN1:sch 1();
now :: thesis: for z being object st z in dom G holds
f1 . z in G . z
let z be object ; :: thesis: ( z in dom G implies f1 . z in G . z )
assume A11: z in dom G ; :: thesis: f1 . z in G . z
A12: now :: thesis: ( z in dom F implies f1 . z in G . z )
assume A13: z in dom F ; :: thesis: f1 . z in G . z
then A14: f1 . z = g . z by A10, A11;
g . z in F . z by A7, A13;
hence f1 . z in G . z by A1, A13, A14, GRFUNC_1:2; :: thesis: verum
end;
( not z in dom F implies f1 . z = h . z ) by A10, A11;
hence f1 . z in G . z by A9, A11, A12; :: thesis: verum
end;
then A15: f1 in product G by A10, Def5;
then A16: f . f1 = f1 | (dom F) by A4;
A17: dom (f1 | (dom F)) = dom F by A2, A10, RELAT_1:62;
now :: thesis: for z being object st z in dom F holds
(f1 | (dom F)) . z = g . z
let z be object ; :: thesis: ( z in dom F implies (f1 | (dom F)) . z = g . z )
assume A18: z in dom F ; :: thesis: (f1 | (dom F)) . z = g . z
then (f1 | (dom F)) . z = f1 . z by A17, FUNCT_1:47;
hence (f1 | (dom F)) . z = g . z by A2, A10, A18; :: thesis: verum
end;
then f . f1 = g by A6, A16, A17, FUNCT_1:2;
hence x in rng f by A4, A5, A15, FUNCT_1:def 3; :: thesis: verum
end;
hence Product F c= Product G by A4, CARD_1:12; :: thesis: verum