let m be Element of NAT ; :: thesis: for I being preProgram of SCM+FSA holds card (ProgramPart (Relocated I,m)) = card I
deffunc H₁( Element of NAT ) -> Element of NAT = $1;
let I be preProgram of SCM+FSA ; :: thesis: card (ProgramPart (Relocated I,m)) = card I
set B = { l where l is Element of NAT : H₁(l) in dom I } ;
A1: for x being set st x in dom I holds
ex d being Element of NAT st x = H₁(d)

proof

let x be set ; :: thesis: ( x in dom I implies ex d being Element of NAT st x = H₁(d) )
assume A2: x in dom I ; :: thesis: ex d being Element of NAT st x = H₁(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 = H₁(d) ;
hence ex d being Element of NAT st x = H₁(d) ; :: thesis: verum

end;

A3: for d1, d2 being Element of NAT st H₁(d1) = H₁(d2) holds
d1 = d2 ;
A4: dom I,{ l where l is Element of NAT : H₁(l) in dom I } are_equipotent from FUNCT_7:sch 3(A1, A3);
defpred S₁[ Element of NAT ] means $1 in dom I;
deffunc H₂( Element of NAT ) -> Element of NAT = $1 + m;
defpred S₂[ Element of NAT ] means H₁($1) in dom I;
set D = { l where l is Element of NAT : S₂[l] } ;
set C = { H₂(l) where l is Element of NAT : l in { l where l is Element of NAT : H₁(l) in dom I } } ;
defpred S₃[ set ] means verum;
{ l where l is Element of NAT : S₂[l] } is Subset of NAT from DOMAIN_1:sch 7();
then A5: { l where l is Element of NAT : H₁(l) in dom I } c= NAT ;
A6: for d1, d2 being Element of NAT st H₂(d1) = H₂(d2) holds
d1 = d2 ;
A7: { l where l is Element of NAT : H₁(l) in dom I } ,{ H₂(l) where l is Element of NAT : l in { l where l is Element of NAT : H₁(l) in dom I } } are_equipotent from FUNCT_7:sch 4(A5, A6);
set C = { H₂(l) where l is Element of NAT : ( l in { n where n is Element of NAT : S₁[n] } & S₃[l] ) } ;
set A = { H₂(l) where l is Element of NAT : ( S₁[l] & S₃[l] ) } ;
A8: { H₂(l) where l is Element of NAT : ( l in { n where n is Element of NAT : S₁[n] } & S₃[l] ) } = { (l + m) where l is Element of NAT : l in { l where l is Element of NAT : H₁(l) in dom I } }

proof

thus { H₂(l) where l is Element of NAT : ( l in { n where n is Element of NAT : S₁[n] } & S₃[l] ) } c= { (l + m) where l is Element of NAT : l in { l where l is Element of NAT : H₁(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 : H₁(l) in dom I } } c= { H₂(l) where l is Element of NAT : ( l in { n where n is Element of NAT : S₁[n] } & S₃[l] ) }

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { H₂(l) where l is Element of NAT : ( l in { n where n is Element of NAT : S₁[n] } & S₃[l] ) } or e in { (l + m) where l is Element of NAT : l in { l where l is Element of NAT : H₁(l) in dom I } } )
assume e in { H₂(l) where l is Element of NAT : ( l in { n where n is Element of NAT : S₁[n] } & S₃[l] ) } ; :: thesis: e in { (l + m) where l is Element of NAT : l in { l where l is Element of NAT : H₁(l) in dom I } }
then ex l being Element of NAT st
( e = H₂(l) & l in { l where l is Element of NAT : H₁(l) in dom I } ) ;
hence e in { (l + m) where l is Element of NAT : l in { l where l is Element of NAT : H₁(l) in dom I } } ; :: thesis: verum

end;

let e be set ; :: 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 : H₁(l) in dom I } } or e in { H₂(l) where l is Element of NAT : ( l in { n where n is Element of NAT : S₁[n] } & S₃[l] ) } )
assume e in { (l + m) where l is Element of NAT : l in { l where l is Element of NAT : H₁(l) in dom I } } ; :: thesis: e in { H₂(l) where l is Element of NAT : ( l in { n where n is Element of NAT : S₁[n] } & S₃[l] ) }
then ex l being Element of NAT st
( e = l + m & l in { l where l is Element of NAT : H₁(l) in dom I } ) ;
hence e in { H₂(l) where l is Element of NAT : ( l in { n where n is Element of NAT : S₁[n] } & S₃[l] ) } ; :: thesis: verum

end;

{ H₂(l) where l is Element of NAT : ( S₁[l] & S₃[l] ) } = { (l + m) where l is Element of NAT : l in dom I }

proof

thus { H₂(l) where l is Element of NAT : ( S₁[l] & S₃[l] ) } c= { (l + m) where l is Element of NAT : l in dom I } :: according to XBOOLE_0:def 10 :: thesis: { (l + m) where l is Element of NAT : l in dom I } c= { H₂(l) where l is Element of NAT : ( S₁[l] & S₃[l] ) }

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in { H₂(l) where l is Element of NAT : ( S₁[l] & S₃[l] ) } or e in { (l + m) where l is Element of NAT : l in dom I } )
assume e in { H₂(l) where l is Element of NAT : ( S₁[l] & S₃[l] ) } ; :: thesis: e in { (l + m) where l is Element of NAT : l in dom I }
then ex l being Element of NAT st
( e = H₂(l) & l in dom I ) ;
hence e in { (l + m) where l is Element of NAT : l in dom I } ; :: thesis: verum

end;

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 { H₂(l) where l is Element of NAT : ( S₁[l] & S₃[l] ) } )
assume e in { (l + m) where l is Element of NAT : l in dom I } ; :: thesis: e in { H₂(l) where l is Element of NAT : ( S₁[l] & S₃[l] ) }
then ex l being Element of NAT st
( e = l + m & l in dom I ) ;
hence e in { H₂(l) where l is Element of NAT : ( S₁[l] & S₃[l] ) } ; :: thesis: verum

end;

then A9: dom (Shift I,m) = { H₂(l) where l is Element of NAT : ( S₁[l] & S₃[l] ) } by VALUED_1:def 12;
{ H₂(l) where l is Element of NAT : ( l in { n where n is Element of NAT : S₁[n] } & S₃[l] ) } = { H₂(l) where l is Element of NAT : ( S₁[l] & S₃[l] ) } from FRAENKEL:sch 14();
then A10: dom (Shift I,m), dom I are_equipotent by A4, A7, A8, A9, WELLORD2:22;
thus card (ProgramPart (Relocated I,m)) = card (Reloc (ProgramPart I),m) by AMISTD_2:69
.= card (Reloc I,m) by RELAT_1:209
.= card (dom (Reloc I,m)) by CARD_1:104
.= card (dom (Shift I,m)) by AMISTD_2:def 15
.= card (dom I) by A10, CARD_1:21
.= card I by CARD_1:104 ; :: thesis: verum