let S be COM-Struct ; :: thesis: for m being Nat
for I being preProgram of S holds card (Reloc (I,m)) = card I
let m be Nat; :: thesis: for I being preProgram of S holds card (Reloc (I,m)) = card I
let I be preProgram of S; :: thesis: card (Reloc (I,m)) = card I
deffunc H1( Nat) -> Nat = $1;
set B = { l where l is Element of NAT : H1(l) in dom 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 d = l as Element of NAT ;
l = H1(d) ;
hence ex d being Element of NAT st x = H1(d) ; :: thesis: verum
end;
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);
 defpred S1[ Nat] means $1 in dom I;
deffunc H2( Nat) -> set = $1 + m;
defpred S2[ Nat] means H1($1) in dom I;
set D = { l where l is Element of NAT : S2[l] } ;
set C = { H2(l) where l is Element of NAT : l in { l where l is Element of NAT : H1(l) in dom I } } ;
defpred S3[ set ] means verum;
{ l where l is Element of NAT : S2[l] } is Subset of NAT from DOMAIN_1:sch 7();
 then A5: { l where l is Element of NAT : H1(l) in dom I } c= NAT ;
A6: for d1, d2 being Element of NAT st H2(d1) = H2(d2) holds
d1 = d2 ;
A7: { l where l is Element of NAT : H1(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(A5, A6);
 set C = { H2(l) where l is Element of NAT : ( l in { n where n is Element of NAT : S1[n] } & S3[l] ) } ;
set A = { H2(l) where l is Element of NAT : ( S1[l] & S3[l] ) } ;
A8: { H2(l) where l is Element of NAT : ( l in { n where n is Element of NAT : S1[n] } & S3[l] ) } = { (l + m) where l is Element of NAT : l in { l where l is Element of NAT : H1(l) in dom I } }
proof
thus { H2(l) where l is Element of NAT : ( l in { n where n is Element of NAT : S1[n] } & S3[l] ) } c= { (l + m) where l is Element of NAT : l in { l where l is Element of NAT : H1(l) in dom I } } :: according to XBOOLE_0:def 10 :: thesis: { (l + m) 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 : S1[n] } & S3[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 { n where n is Element of NAT : S1[n] } & S3[l] ) } or e in { (l + m) where l is Element of NAT : l in { l where l is Element of NAT : H1(l) in dom I } } )
assume e in { H2(l) where l is Element of NAT : ( l in { n where n is Element of NAT : S1[n] } & S3[l] ) } ; :: thesis: e in { (l + m) where l is Element of NAT : l in { l where l is Element of NAT : H1(l) in dom I } }
then ex l being Element of NAT st
( e = H2(l) & l in { l where l is Element of NAT : H1(l) in dom I } ) ;
hence e in { (l + m) where l is Element of NAT : l in { l where l is Element of NAT : H1(l) in dom I } } ; :: thesis: verum
end;
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { (l + m) 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 : S1[n] } & S3[l] ) } )
assume e in { (l + m) 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 : S1[n] } & S3[l] ) }
then ex l being Element of NAT st
( e = l + m & l in { l where l is Element of NAT : H1(l) in dom I } ) ;
hence e in { H2(l) where l is Element of NAT : ( l in { n where n is Element of NAT : S1[n] } & S3[l] ) } ; :: thesis: verum
end;
{ H2(l) where l is Element of NAT : ( S1[l] & S3[l] ) } = { (l + m) where l is Nat : l in dom I }
proof
thus { H2(l) where l is Element of NAT : ( S1[l] & S3[l] ) } c= { (l + m) where l is Nat : l in dom I } :: according to XBOOLE_0:def 10 :: thesis: { (l + m) where l is Nat : l in dom I } c= { H2(l) where l is Element of NAT : ( S1[l] & S3[l] ) }
proof
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { H2(l) where l is Element of NAT : ( S1[l] & S3[l] ) } or e in { (l + m) where l is Nat : l in dom I } )
assume e in { H2(l) where l is Element of NAT : ( S1[l] & S3[l] ) } ; :: thesis: e in { (l + m) where l is Nat : l in dom I }
then ex l being Element of NAT st
( e = H2(l) & l in dom I ) ;
hence e in { (l + m) where l is Nat : l in dom I } ; :: thesis: verum
end;
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 : ( S1[l] & S3[l] ) } )
assume e in { (l + m) where l is Nat : l in dom I } ; :: thesis: e in { H2(l) where l is Element of NAT : ( S1[l] & S3[l] ) }
then consider l being Nat such that
A9: ( e = l + m & l in dom I ) ;
reconsider l = l as Element of NAT by ORDINAL1:def 12;
l in dom I by A9;
hence e in { H2(l) where l is Element of NAT : ( S1[l] & S3[l] ) } by A9; :: thesis: verum
end;
then A10: dom (Shift (I,m)) = { H2(l) where l is Element of NAT : ( S1[l] & S3[l] ) } by VALUED_1:def 12;
{ H2(l) where l is Element of NAT : ( l in { n where n is Element of NAT : S1[n] } & S3[l] ) } = { H2(l) where l is Element of NAT : ( S1[l] & S3[l] ) } from FRAENKEL:sch 14();
 then A11: dom (Shift (I,m)), dom I are_equipotent by A4, A7, A8, A10, WELLORD2:15;
thus card (Reloc (I,m)) = card (dom (Reloc (I,m))) by CARD_1:62
.= card (dom (Shift (I,m))) by Th20
.= card (dom I) by A11, CARD_1:5
.= card I by CARD_1:62 ; :: thesis: verum