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

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

hence
(k (#) (l GeoSeq)) | m is XFinSequence of NAT
by RELAT_1:def 19; :: thesis: verum
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;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