let X be set ; :: thesis: for f being X -defined Function
for perm being Permutation of X holds card (support (f * perm)) = card (support f)
let f be X -defined Function; :: thesis: for perm being Permutation of X holds card (support (f * perm)) = card (support f)
let perm be Permutation of X; :: thesis: card (support (f * perm)) = card (support f)
set P = perm " ;
A1: ( dom perm = X & X = rng perm & dom (perm ") = X & X = rng (perm ") ) by FUNCT_2:52, FUNCT_2:def 3;
( support f c= dom f & dom f c= X & X = dom (perm ") ) by FUNCT_2:52, PRE_POLY:37;
then A2: support f c= dom (perm ") ;
A3: (perm ") .: (support f) c= support (f * perm)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (perm ") .: (support f) or y in support (f * perm) )
assume y in (perm ") .: (support f) ; :: thesis: y in support (f * perm)
then consider x being object such that
A4: ( x in dom (perm ") & x in support f & (perm ") . x = y ) by FUNCT_1:def 6;
A5: x = perm . y by A1, A4, FUNCT_1:32;
A6: f . x <> 0 by A4, PRE_POLY:def 7;
then ( x in dom f & y in dom perm ) by A4, A1, FUNCT_1:def 2, FUNCT_1:def 3;
then ( perm . y in dom f & f . (perm . y) = (f * perm) . y ) by A1, A4, FUNCT_1:32, FUNCT_1:13;
hence y in support (f * perm) by A6, A5, PRE_POLY:def 7; :: thesis: verum

end;

support (f * perm) c= (perm ") .: (support f)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in support (f * perm) or y in (perm ") .: (support f) )
assume y in support (f * perm) ; :: thesis: y in (perm ") .: (support f)
then A7: (f * perm) . y <> 0 by PRE_POLY:def 7;
then y in dom (f * perm) by FUNCT_1:def 2;
then ( f . (perm . y) = (f * perm) . y & y in dom perm & perm . y in dom f ) by FUNCT_1:11, FUNCT_1:12;
then ( perm . y in dom (perm ") & perm . y in support f & (perm ") . (perm . y) = y ) by A1, A7, FUNCT_1:32, PRE_POLY:def 7;
hence y in (perm ") .: (support f) by FUNCT_1:def 6; :: thesis: verum

end;

then support (f * perm) = (perm ") .: (support f) by A3, XBOOLE_0:def 10;
hence card (support (f * perm)) = card (support f) by CARD_1:5, A2, CARD_1:33; :: thesis: verum