A1: dom (f to_power g) = (dom f) /\ (dom g) by Def6;
A2: n in NAT by ORDINAL1:def 12;
( len f = n & len g = n ) by CARD_1:def 7;
then ( dom f = Seg n & dom g = Seg n ) by FINSEQ_1:def 3;
hence f to_power g is n -element by A1, A2, FINSEQ_1:def 3; :: thesis: verum