let X be set ; :: thesis: for fs being FinSequence of X

for fss being Subset of fs

for m being Element of NAT st m in dom (Seq fss) holds

ex n being Element of NAT st

( n in dom fs & m <= n & (Seq fss) . m = fs . n )

let fs be FinSequence of X; :: thesis: for fss being Subset of fs

for m being Element of NAT st m in dom (Seq fss) holds

ex n being Element of NAT st

( n in dom fs & m <= n & (Seq fss) . m = fs . n )

let fss be Subset of fs; :: thesis: for m being Element of NAT st m in dom (Seq fss) holds

ex n being Element of NAT st

( n in dom fs & m <= n & (Seq fss) . m = fs . n )

let m be Element of NAT ; :: thesis: ( m in dom (Seq fss) implies ex n being Element of NAT st

( n in dom fs & m <= n & (Seq fss) . m = fs . n ) )

set f = Sgm (dom fss);

set n = (Sgm (dom fss)) . m;

consider k being Nat such that

A1: dom fss c= Seg k by FINSEQ_1:def 12;

assume A2: m in dom (Seq fss) ; :: thesis: ex n being Element of NAT st

( n in dom fs & m <= n & (Seq fss) . m = fs . n )

then A3: m in dom (fss * (Sgm (dom fss))) by FINSEQ_1:def 14;

then A4: (Sgm (dom fss)) . m in dom fss by FUNCT_1:11;

Seq fss = fss * (Sgm (dom fss)) by FINSEQ_1:def 14;

then (Seq fss) . m = fss . ((Sgm (dom fss)) . m) by A2, FUNCT_1:12;

then A5: [((Sgm (dom fss)) . m),((Seq fss) . m)] in fss by A4, FUNCT_1:def 2;

then A6: (Sgm (dom fss)) . m in dom fs by FUNCT_1:1;

A7: m in dom (Sgm (dom fss)) by A3, FUNCT_1:11;

A8: (Seq fss) . m = fs . ((Sgm (dom fss)) . m) by A5, FUNCT_1:1;

k in NAT by ORDINAL1:def 12;

hence ex n being Element of NAT st

( n in dom fs & m <= n & (Seq fss) . m = fs . n ) by A7, A6, A8, A1, FINSEQ_3:152; :: thesis: verum

for fss being Subset of fs

for m being Element of NAT st m in dom (Seq fss) holds

ex n being Element of NAT st

( n in dom fs & m <= n & (Seq fss) . m = fs . n )

let fs be FinSequence of X; :: thesis: for fss being Subset of fs

for m being Element of NAT st m in dom (Seq fss) holds

ex n being Element of NAT st

( n in dom fs & m <= n & (Seq fss) . m = fs . n )

let fss be Subset of fs; :: thesis: for m being Element of NAT st m in dom (Seq fss) holds

ex n being Element of NAT st

( n in dom fs & m <= n & (Seq fss) . m = fs . n )

let m be Element of NAT ; :: thesis: ( m in dom (Seq fss) implies ex n being Element of NAT st

( n in dom fs & m <= n & (Seq fss) . m = fs . n ) )

set f = Sgm (dom fss);

set n = (Sgm (dom fss)) . m;

consider k being Nat such that

A1: dom fss c= Seg k by FINSEQ_1:def 12;

assume A2: m in dom (Seq fss) ; :: thesis: ex n being Element of NAT st

( n in dom fs & m <= n & (Seq fss) . m = fs . n )

then A3: m in dom (fss * (Sgm (dom fss))) by FINSEQ_1:def 14;

then A4: (Sgm (dom fss)) . m in dom fss by FUNCT_1:11;

Seq fss = fss * (Sgm (dom fss)) by FINSEQ_1:def 14;

then (Seq fss) . m = fss . ((Sgm (dom fss)) . m) by A2, FUNCT_1:12;

then A5: [((Sgm (dom fss)) . m),((Seq fss) . m)] in fss by A4, FUNCT_1:def 2;

then A6: (Sgm (dom fss)) . m in dom fs by FUNCT_1:1;

A7: m in dom (Sgm (dom fss)) by A3, FUNCT_1:11;

A8: (Seq fss) . m = fs . ((Sgm (dom fss)) . m) by A5, FUNCT_1:1;

k in NAT by ORDINAL1:def 12;

hence ex n being Element of NAT st

( n in dom fs & m <= n & (Seq fss) . m = fs . n ) by A7, A6, A8, A1, FINSEQ_3:152; :: thesis: verum