let m be Element of NAT ; :: thesis: { a where a is Nat : a < m } is_CRS_of m
deffunc H₁( Nat) -> Element of NAT = $1 -' 1;
consider fp being FinSequence such that
A1: ( len fp = m & ( for a being Nat st a in dom fp holds
fp . a = H₁(a) ) ) from FINSEQ_1:sch 2();
for a being Nat st a in dom fp holds
fp . a in INT

proof

let a be Nat; :: thesis: ( a in dom fp implies fp . a in INT )
assume a in dom fp ; :: thesis: fp . a in INT
then fp . a = H₁(a) by A1;
hence fp . a in INT by INT_1:def 2; :: thesis: verum

end;

then reconsider fp = fp as FinSequence of INT by FINSEQ_2:12;
A2: { a where a is Nat : a < m } = rng fp

proof

set A = { a where a is Nat : a < m } ;
A3: rng fp c= { a where a is Nat : a < m }

proof

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in rng fp or b in { a where a is Nat : a < m } )
assume b in rng fp ; :: thesis: b in { a where a is Nat : a < m }
then consider k being object such that
A4: k in dom fp and
A5: b = fp . k by FUNCT_1:def 3;
reconsider k = k as Element of NAT by A4;
A6: k in Seg m by A1, A4, FINSEQ_1:def 3;
then k <= m by FINSEQ_1:1;
then A7: k - 1 < m by XREAL_1:147;
k >= 1 by A6, FINSEQ_1:1;
then A8: k -' 1 < m by A7, XREAL_1:233;
reconsider b = b as Integer by A5;
b = k -' 1 by A1, A4, A5;
hence b in { a where a is Nat : a < m } by A8; :: thesis: verum

end;

{ a where a is Nat : a < m } c= rng fp

proof

let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in { a where a is Nat : a < m } or b in rng fp )
assume b in { a where a is Nat : a < m } ; :: thesis: b in rng fp
then consider k being Nat such that
A9: k = b and
A10: k < m ;
( k + 1 >= 1 & k + 1 <= m ) by A10, NAT_1:11, NAT_1:13;
then A11: k + 1 in dom fp by A1, FINSEQ_3:25;
then fp . (k + 1) = (k + 1) -' 1 by A1
.= k by NAT_D:34 ;
hence b in rng fp by A9, A11, FUNCT_1:def 3; :: thesis: verum

end;

hence { a where a is Nat : a < m } = rng fp by A3; :: thesis: verum

end;

for a being Nat st a in dom fp holds
fp . a in Class ((Cong m),(a -' 1))

proof

let a be Nat; :: thesis: ( a in dom fp implies fp . a in Class ((Cong m),(a -' 1)) )
a -' 1,a -' 1 are_congruent_mod m by INT_1:11;
then A12: [(a -' 1),(a -' 1)] in Cong m by Def1;
assume a in dom fp ; :: thesis: fp . a in Class ((Cong m),(a -' 1))
then fp . a = a -' 1 by A1;
hence fp . a in Class ((Cong m),(a -' 1)) by A12, EQREL_1:18; :: thesis: verum

end;

hence { a where a is Nat : a < m } is_CRS_of m by A1, A2; :: thesis: verum