let X be set ; for f being Function holds product (Funcs (X,f)), Funcs (X,(product f)) are_equipotent
let f be Function; product (Funcs (X,f)), Funcs (X,(product f)) are_equipotent
A1:
Funcs (X,(product {})) = {(X --> {})}
by CARD_3:19, FUNCT_5:66;
A2: product (Funcs ({},f)) =
product ((dom f) --> {{}})
by Th78
.=
Funcs ((dom f),{{}})
by CARD_3:20
.=
{((dom f) --> {})}
by FUNCT_5:66
;
A3:
( Funcs ({},(product f)) = {{}} & product (Funcs (X,{})) = {{}} )
by Th79, CARD_3:19, FUNCT_5:64;
( X <> {} & f <> {} implies product (Funcs (X,f)), Funcs (X,(product f)) are_equipotent )
by Lm5;
hence
product (Funcs (X,f)), Funcs (X,(product f)) are_equipotent
by A2, A3, A1, CARD_1:48; verum