let m be Element of NAT ; :: thesis: { a where a is Nat : a < m } is_CRS_of m

deffunc H_{1}( 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_{1}(a) ) )
from FINSEQ_1:sch 2();

for a being Nat st a in dom fp holds

fp . a in INT

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

fp . a in Class ((Cong m),(a -' 1))

deffunc H

consider fp being FinSequence such that

A1: ( len fp = m & ( for a being Nat st a in dom fp holds

fp . a = H

for a being Nat st a in dom fp holds

fp . a in INT

proof

then reconsider fp = fp as FinSequence of INT by FINSEQ_2:12;
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_{1}(a)
by A1;

hence fp . a in INT by INT_1:def 2; :: thesis: verum

end;assume a in dom fp ; :: thesis: fp . a in INT

then fp . a = H

hence fp . a in INT by INT_1:def 2; :: thesis: verum

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

proof

for a being Nat st a in dom fp holds
set A = { a where a is Nat : a < m } ;

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

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

proof

{ a where a is Nat : a < m } c= rng fp
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;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

proof

hence
{ a where a is Nat : a < m } = rng fp
by A3; :: thesis: verum
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;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

fp . a in Class ((Cong m),(a -' 1))

proof

hence
{ a where a is Nat : a < m } is_CRS_of m
by A1, A2; :: thesis: verum
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;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