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 13;
then m c= dom (k (#) (l GeoSeq )) by A1, ORDINAL1:def 2;
then dom ((k (#) (l GeoSeq )) | m) = m by RELAT_1:91;
then reconsider g9 = (k (#) (l GeoSeq )) | m as XFinSequence by ORDINAL1:def 7;
rng g9 c= NAT

proof

let a be set ; :: 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 set such that
A2: o in dom ((k (#) (l GeoSeq )) | m) and
A3: a = ((k (#) (l GeoSeq )) | m) . o by FUNCT_1:def 5;
reconsider o = o as Element of NAT by A2;
((k (#) (l GeoSeq )) | m) . o = (k (#) (l GeoSeq )) . o by A2, FUNCT_1:70
.= k * ((l GeoSeq ) . o) by SEQ_1:13
.= k * (l |^ o) by PREPOWER:def 1 ;
hence a in NAT by A3; :: thesis: verum

end;

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