let f, g be Function; :: thesis: ( dom f, dom g are_equipotent iff f,g are_equipotent )
A1: ( card f = card (dom f) & card g = card (dom g) ) by CARD_1:62;
hereby :: thesis: ( f,g are_equipotent implies dom f, dom g are_equipotent )
assume dom f, dom g are_equipotent ; :: thesis: f,g are_equipotent
then card (dom f) = card (dom g) by CARD_1:5;
hence f,g are_equipotent by A1, CARD_1:5; :: thesis: verum
end;
assume f,g are_equipotent ; :: thesis: dom f, dom g are_equipotent
then card f = card g by CARD_1:5;
hence dom f, dom g are_equipotent by A1, CARD_1:5; :: thesis: verum