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