deffunc H1( Nat) -> FinSeq-Location = fsloc c1;
consider f being sequence of the carrier of SCM+FSA such that
A1: for k being Element of NAT holds f . k = H1(k) from FUNCT_2:sch 4();
 NAT , FinSeq-Locations are_equipotent
proof
take f ; :: according to WELLORD2:def 4 :: thesis: ( f is one-to-one & proj1 f = NAT & proj2 f = FinSeq-Locations )
thus f is one-to-one :: thesis: ( proj1 f = NAT & proj2 f = FinSeq-Locations )
proof
let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume that
A2: ( x1 in dom f & x2 in dom f ) and
A3: f . x1 = f . x2 ; :: thesis: x1 = x2
reconsider k1 = x1, k2 = x2 as Element of NAT by A2;
fsloc k1 = f . k1 by A1
.= fsloc k2 by A1, A3 ;
hence x1 = x2 ; :: thesis: verum
end;
thus dom f = NAT by FUNCT_2:def 1; :: thesis: proj2 f = FinSeq-Locations
thus rng f c= FinSeq-Locations :: according to XBOOLE_0:def 10 :: thesis: FinSeq-Locations c= proj2 f
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in FinSeq-Locations )
assume y in rng f ; :: thesis: y in FinSeq-Locations
then consider x being object such that
A4: x in dom f and
A5: y = f . x by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A4;
y = fsloc x by A1, A5;
hence y in FinSeq-Locations by Def3; :: thesis: verum
end;
thus FinSeq-Locations c= rng f :: thesis: verum
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in FinSeq-Locations or y in rng f )
assume y in FinSeq-Locations ; :: thesis: y in rng f
then y is FinSeq-Location by Def3;
then consider i being Nat such that
A6: y = fsloc i by Th4;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
i in NAT ;
then A7: i in dom f by FUNCT_2:def 1;
y = f . i by A1, A6;
hence y in rng f by A7, FUNCT_1:def 3; :: thesis: verum
end;
end;
hence not FinSeq-Locations is finite by CARD_1:38; :: thesis: verum