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 object ; :: 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 object such that
A1: x in dom c and
A2: y = c . x by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A1;
( 1 <= x & x <= len c ) by A1, FINSEQ_3:25;
hence y in the carrier' of G by A2, Def14; :: thesis: verum
end;
hence c is FinSequence of the carrier' of G by FINSEQ_1:def 4; :: thesis: verum