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)
proof
let x be set ; :: thesis: ( x in dom I implies ex d being Element of NAT st x = H1(d) )
assume A2: x in dom I ; :: thesis: ex d being Element of NAT st x = H1(d)
dom I c= NAT by RELAT_1:def 18;
then reconsider l = x as Element of NAT by A2;
reconsider l = l as Element of NAT ;
take l ; :: thesis: x = H1(l)
thus x = H1(l) ; :: thesis: verum
end;
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 } ;
A3: for d1, d2 being Element of NAT st H1(d1) = H1(d2) holds
d1 = d2 ;
A4: dom I, { l where l is Element of NAT : H1(l) in dom I } are_equipotent from FUNCT_7:sch 3(A1, A3);
 A5: { 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
A6: e = H2(l) and
A7: ( 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 A7;
hence e in { (l + m) where l is Element of NAT : l in dom I } by A6; :: 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 A8: { l where l is Element of NAT : S2[l] } c= NAT ;
set B = { l where l is Element of NAT : l in dom I } ;
A9: for d1, d2 being Element of NAT st H2(d1) = H2(d2) holds
d1 = d2 ;
A10: { 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(A8, A9);
 A11: { (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
A12: e = l + m and
A13: l in dom I ;
l in { l where l is Element of NAT : l in dom I } by A13;
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 A12; :: thesis: verum
end;
A14: dom (Shift (I,m)) = { (l + m) where l is Element of NAT : l in dom I } by VALUED_1:def 12;
A15: { 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 A11, XBOOLE_1:1;
then A16: { 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 A5, 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 A11, A15, XBOOLE_0:def 10;
then A17: dom (Shift (I,m)), dom I are_equipotent by A4, A16, A10, A14, WELLORD2:15;
thus card (Shift (I,m)) = card (dom (Shift (I,m))) by CARD_1:62
.= card (dom I) by A17, CARD_1:5
.= card I by CARD_1:62 ; :: thesis: verum