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