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:10, FUNCT_5:59;
A2: product (Funcs ({},f)) =
product ((dom f) --> {{}})
by Th45
.=
Funcs ((dom f),{{}})
by CARD_3:11
.=
{((dom f) --> {})}
by FUNCT_5:59
;
A3:
( Funcs ({},(product f)) = {{}} & product (Funcs (X,{})) = {{}} )
by Th46, CARD_3:10, FUNCT_5:57;
( X <> {} & f <> {} implies product (Funcs (X,f)), Funcs (X,(product f)) are_equipotent )
by Lm4;
hence
product (Funcs (X,f)), Funcs (X,(product f)) are_equipotent
by A2, A3, A1, CARD_1:28; verum