let c be Chain of G; :: thesis: c is FinSequence of the carrier' of G
A1: 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 A2: y in rng c ; :: thesis: y in the carrier' of G
consider x being set such that
A3: x in dom c and
A4: y = c . x by A2, FUNCT_1:def 5;
reconsider x = x as Element of NAT by A3;
A5: ( 1 <= x & x <= len c ) by A3, FINSEQ_3:27;
thus y in the carrier' of G by A4, A5, Def12; :: thesis: verum

end;

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