let f be Function; :: thesis: for p being Permutation of (dom f) holds Card (f * p) = (Card f) * p
let p be Permutation of (dom f); :: thesis: Card (f * p) = (Card f) * p
A1: rng p = dom f by FUNCT_2:def 3;
then A2: rng p = dom (Card f) by CARD_3:def 2;
A3: dom (Card (f * p)) = dom (f * p) by CARD_3:def 2
.= dom p by A1, RELAT_1:27
.= dom ((Card f) * p) by A2, RELAT_1:27 ;
now :: thesis: for x being object st x in dom (Card (f * p)) holds
(Card (f * p)) . x = ((Card f) * p) . x
let x be object ; :: thesis: ( x in dom (Card (f * p)) implies (Card (f * p)) . x = ((Card f) * p) . x )
assume A4: x in dom (Card (f * p)) ; :: thesis: (Card (f * p)) . x = ((Card f) * p) . x
then A5: x in dom (f * p) by CARD_3:def 2;
then A6: p . x in dom f by FUNCT_1:11;
thus (Card (f * p)) . x = card ((f * p) . x) by A5, CARD_3:def 2
.= card (f . (p . x)) by A5, FUNCT_1:12
.= (Card f) . (p . x) by A6, CARD_3:def 2
.= ((Card f) * p) . x by A3, A4, FUNCT_1:12 ; :: thesis: verum
end;
hence Card (f * p) = (Card f) * p by A3, FUNCT_1:2; :: thesis: verum