let c be Chain of G; :: thesis: c is FinSequence of the carrier' of G
rng c c= the carrier' of G

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng c or y in the carrier' of G )
assume y in rng c ; :: thesis: y in the carrier' of G
then consider x being set such that
A3: x in dom c and
A4: y = c . x by FUNCT_1:def 5;
reconsider x = x as Element of NAT by A3;
( 1 <= x & x <= len c ) by A3, FINSEQ_3:27;
hence y in the carrier' of G by A4, Def12; :: thesis: verum

end;

hence c is FinSequence of the carrier' of G by FINSEQ_1:def 4; :: thesis: verum