let m be Element of NAT ; :: thesis: for I being NAT -defined Function holds card (Shift (I,m)) = card I
defpred S1[ set ] means verum;
deffunc H1( Element of NAT ) -> Element of NAT = $1;
let I be NAT -defined Function; :: thesis: card (Shift (I,m)) = card I
A1: for x being set st x in dom I holds
ex d being Element of NAT st x = H1(d) ;
defpred S2[ Element of NAT ] means $1 in dom I;
deffunc H2( Element of NAT ) -> Element of NAT = $1 + m;
set B = { l where l is Element of NAT : H1(l) in dom I } ;
set C = { H2(l) where l is Element of NAT : ( l in { n where n is Element of NAT : S2[n] } & S1[l] ) } ;
set D = { H2(l) where l is Element of NAT : l in { l where l is Element of NAT : H1(l) in dom I } } ;
set E = { (l + m) where l is Element of NAT : l in dom I } ;
A2: for d1, d2 being Element of NAT st H1(d1) = H1(d2) holds
d1 = d2 ;
A3: dom I, { l where l is Element of NAT : H1(l) in dom I } are_equipotent from FUNCT_7:sch 3(A1, A2);
 A4: { H2(l) where l is Element of NAT : ( l in { n where n is Element of NAT : S2[n] } & S1[l] ) } c= { (l + m) where l is Element of NAT : l in dom I }
proof
let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { H2(l) where l is Element of NAT : ( l in { n where n is Element of NAT : S2[n] } & S1[l] ) } or e in { (l + m) where l is Element of NAT : l in dom I } )
assume e in { H2(l) where l is Element of NAT : ( l in { n where n is Element of NAT : S2[n] } & S1[l] ) } ; :: thesis: e in { (l + m) where l is Element of NAT : l in dom I }
then consider l being Element of NAT such that
A5: e = H2(l) and
A6: ( l in { n where n is Element of NAT : S2[n] } & S1[l] ) ;
ex n being Element of NAT st
( n = l & S2[n] ) by A6;
hence e in { (l + m) where l is Element of NAT : l in dom I } by A5; :: thesis: verum
end;
set B = { l where l is Element of NAT : S2[l] } ;
{ l where l is Element of NAT : S2[l] } is Subset of NAT from DOMAIN_1:sch 7();
 then A7: { l where l is Element of NAT : S2[l] } c= NAT ;
set B = { l where l is Element of NAT : l in dom I } ;
A8: for d1, d2 being Element of NAT st H2(d1) = H2(d2) holds
d1 = d2 ;
A9: { l where l is Element of NAT : l in dom I } , { H2(l) where l is Element of NAT : l in { l where l is Element of NAT : H1(l) in dom I } } are_equipotent from FUNCT_7:sch 4(A7, A8);
 A10: { (l + m) where l is Element of NAT : l in dom I } c= { H2(l) where l is Element of NAT : l in { l where l is Element of NAT : H1(l) in dom I } }
proof
let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { (l + m) where l is Element of NAT : l in dom I } or e in { H2(l) where l is Element of NAT : l in { l where l is Element of NAT : H1(l) in dom I } } )
assume e in { (l + m) where l is Element of NAT : l in dom I } ; :: thesis: e in { H2(l) where l is Element of NAT : l in { l where l is Element of NAT : H1(l) in dom I } }
then consider l being Element of NAT such that
A11: e = l + m and
A12: l in dom I ;
l in { l where l is Element of NAT : l in dom I } by A12;
hence e in { H2(l) where l is Element of NAT : l in { l where l is Element of NAT : H1(l) in dom I } } by A11; :: thesis: verum
end;
A13: dom (Shift (I,m)) = { (l + m) where l is Element of NAT : l in dom I } by VALUED_1:def 12;
A14: { H2(l) where l is Element of NAT : l in { l where l is Element of NAT : H1(l) in dom I } } c= { H2(l) where l is Element of NAT : ( l in { n where n is Element of NAT : S2[n] } & S1[l] ) }
proof
let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { H2(l) where l is Element of NAT : l in { l where l is Element of NAT : H1(l) in dom I } } or e in { H2(l) where l is Element of NAT : ( l in { n where n is Element of NAT : S2[n] } & S1[l] ) } )
assume e in { H2(l) where l is Element of NAT : l in { l where l is Element of NAT : H1(l) in dom I } } ; :: thesis: e in { H2(l) where l is Element of NAT : ( l in { n where n is Element of NAT : S2[n] } & S1[l] ) }
then ex l being Element of NAT st
( e = H2(l) & l in { l where l is Element of NAT : l in dom I } ) ;
hence e in { H2(l) where l is Element of NAT : ( l in { n where n is Element of NAT : S2[n] } & S1[l] ) } ; :: thesis: verum
end;
then { (l + m) where l is Element of NAT : l in dom I } c= { H2(l) where l is Element of NAT : ( l in { n where n is Element of NAT : S2[n] } & S1[l] ) } by A10, XBOOLE_1:1;
then A15: { H2(l) where l is Element of NAT : ( l in { n where n is Element of NAT : S2[n] } & S1[l] ) } = { (l + m) where l is Element of NAT : l in dom I } by A4, XBOOLE_0:def 10;
then { H2(l) where l is Element of NAT : ( l in { n where n is Element of NAT : S2[n] } & S1[l] ) } = { H2(l) where l is Element of NAT : l in { l where l is Element of NAT : H1(l) in dom I } } by A10, A14, XBOOLE_0:def 10;
then A16: dom (Shift (I,m)), dom I are_equipotent by A3, A15, A9, A13, WELLORD2:15;
thus card (Shift (I,m)) = card (dom (Shift (I,m))) by CARD_1:62
.= card (dom I) by A16, CARD_1:5
.= card I by CARD_1:62 ; :: thesis: verum