let m be Nat; :: thesis: for I being NAT -defined Function holds card (Shift (I,m)) = card I
defpred S1[ set ] means verum;
deffunc H1( Nat) -> 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[ Nat] means $1 in dom I;
deffunc H2( Nat) -> set = $1 + m;
set B = { l where l is Element of NAT : H1(l) in dom I } ;
set C = { H2(l) where l is Nat : ( l in { n where n is 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 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 Nat : ( l in { n where n is Nat : S2[n] } & S1[l] ) } c= { (l + m) where l is Nat : l in dom I }
proof
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { H2(l) where l is Nat : ( l in { n where n is Nat : S2[n] } & S1[l] ) } or e in { (l + m) where l is Nat : l in dom I } )
assume e in { H2(l) where l is Nat : ( l in { n where n is Nat : S2[n] } & S1[l] ) } ; :: thesis: e in { (l + m) where l is Nat : l in dom I }
then consider l being Nat such that
A5: e = H2(l) and
A6: ( l in { n where n is Nat : S2[n] } & S1[l] ) ;
ex n being Nat st
( n = l & S2[n] ) by A6;
hence e in { (l + m) where l is 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 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 object ; :: according to TARSKI:def 3 :: thesis: ( not e in { (l + m) where l is 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 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 Nat such that
A11: e = l + m and
A12: l in dom I ;
reconsider l = l as Element of NAT by ORDINAL1:def 12;
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 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 Nat : ( l in { n where n is Nat : S2[n] } & S1[l] ) }
proof
let e be object ; :: 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 Nat : ( l in { n where n is 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 Nat : ( l in { n where n is Nat : S2[n] } & S1[l] ) }
then consider l1 being Element of NAT such that
A15: e = H2(l1) and
A16: l1 in { l where l is Element of NAT : l in dom I } ;
ex l being Element of NAT st
( l1 = l & H1(l) in dom I ) by A16;
then l1 in dom I ;
then l1 in { n where n is Nat : S2[n] } ;
hence e in { H2(l) where l is Nat : ( l in { n where n is Nat : S2[n] } & S1[l] ) } by A15; :: thesis: verum
end;
then { (l + m) where l is Nat : l in dom I } c= { H2(l) where l is Nat : ( l in { n where n is Nat : S2[n] } & S1[l] ) } by A10;
then A17: { H2(l) where l is Nat : ( l in { n where n is Nat : S2[n] } & S1[l] ) } = { (l + m) where l is Nat : l in dom I } by A4;
then { H2(l) where l is Nat : ( l in { n where n is 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;
then A18: dom (Shift (I,m)), dom I are_equipotent by A3, A17, A9, A13, WELLORD2:15;
thus card (Shift (I,m)) = card (dom (Shift (I,m))) by CARD_1:62
.= card (dom I) by A18, CARD_1:5
.= card I by CARD_1:62 ; :: thesis: verum