let X be set ; :: thesis: for k being Nat st X c= Seg k holds
rng (Sgm X) c= Seg k
let k be Nat; :: thesis: ( X c= Seg k implies rng (Sgm X) c= Seg k )
assume A1: X c= Seg k ; :: thesis: rng (Sgm X) c= Seg k
for x being object st x in rng (Sgm X) holds
x in Seg k

proof

let x be object ; :: thesis: ( x in rng (Sgm X) implies x in Seg k )
assume A2: x in rng (Sgm X) ; :: thesis: x in Seg k
X is included_in_Seg by A1, FINSEQ_1:def 13;
then rng (Sgm X) = X by FINSEQ_1:def 14;
hence x in Seg k by A1, A2; :: thesis: verum

end;

hence rng (Sgm X) c= Seg k ; :: thesis: verum