let D be non empty set ; :: thesis: for Y being with_non-empty_element FinSequenceSet of D
for s being non-empty sequence of Y
for s1 being sequence of D st ( for n being Nat holds s1 . n = (joined_seq s) . (((Partial_Sums (Length s)) . n) - 1) ) holds
s1 is subsequence of joined_seq s
let Y be with_non-empty_element FinSequenceSet of D; :: thesis: for s being non-empty sequence of Y
for s1 being sequence of D st ( for n being Nat holds s1 . n = (joined_seq s) . (((Partial_Sums (Length s)) . n) - 1) ) holds
s1 is subsequence of joined_seq s
let s be non-empty sequence of Y; :: thesis: for s1 being sequence of D st ( for n being Nat holds s1 . n = (joined_seq s) . (((Partial_Sums (Length s)) . n) - 1) ) holds
s1 is subsequence of joined_seq s
let s1 be sequence of D; :: thesis: ( ( for n being Nat holds s1 . n = (joined_seq s) . (((Partial_Sums (Length s)) . n) - 1) ) implies s1 is subsequence of joined_seq s )
assume A1: for n being Nat holds s1 . n = (joined_seq s) . (((Partial_Sums (Length s)) . n) - 1) ; :: thesis: s1 is subsequence of joined_seq s
consider N being increasing sequence of NAT such that
A2: for n being Nat holds N . n = ((Partial_Sums (Length s)) . n) - 1 by Th11;
for n being Element of NAT holds s1 . n = ((joined_seq s) * N) . n

proof

let n be Element of NAT ; :: thesis: s1 . n = ((joined_seq s) * N) . n
s1 . n = (joined_seq s) . (((Partial_Sums (Length s)) . n) - 1) by A1;
then s1 . n = (joined_seq s) . (N . n) by A2;
hence s1 . n = ((joined_seq s) * N) . n by FUNCT_2:15; :: thesis: verum

end;

hence s1 is subsequence of joined_seq s by FUNCT_2:def 8; :: thesis: verum