let k, l, m be Nat; :: thesis: (k (#) (l GeoSeq)) | m is XFinSequence of NAT
set g = (k (#) (l GeoSeq)) | m;
A1: dom (k (#) (l GeoSeq)) = NAT by FUNCT_2:def 1;
then m in dom (k (#) (l GeoSeq)) by ORDINAL1:def 12;
then m c= dom (k (#) (l GeoSeq)) by A1, ORDINAL1:def 2;
then dom ((k (#) (l GeoSeq)) | m) = m by RELAT_1:62;
then reconsider g9 = (k (#) (l GeoSeq)) | m as XFinSequence by ORDINAL1:def 7;
rng g9 c= NAT

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng g9 or a in NAT )
assume a in rng g9 ; :: thesis: a in NAT
then consider o being object such that
A2: o in dom ((k (#) (l GeoSeq)) | m) and
A3: a = ((k (#) (l GeoSeq)) | m) . o by FUNCT_1:def 3;
o in dom (k (#) (l GeoSeq)) by A2, RELAT_1:57;
then reconsider o = o as Element of NAT ;
A4: k * (l |^ o) in NAT by ORDINAL1:def 12;
((k (#) (l GeoSeq)) | m) . o = (k (#) (l GeoSeq)) . o by A2, FUNCT_1:47
.= k * ((l GeoSeq) . o) by SEQ_1:9
.= k * (l |^ o) by PREPOWER:def 1 ;
hence a in NAT by A3, A4; :: thesis: verum

end;

hence (k (#) (l GeoSeq)) | m is XFinSequence of NAT by RELAT_1:def 19; :: thesis: verum