let D be non empty set ; :: thesis: for f being FinSequence of D
for G being Matrix of D
for p being Element of D st p in rng f & f is_sequence_on G holds
f :- p is_sequence_on G
let f be FinSequence of D; :: thesis: for G being Matrix of D
for p being Element of D st p in rng f & f is_sequence_on G holds
f :- p is_sequence_on G
let G be Matrix of D; :: thesis: for p being Element of D st p in rng f & f is_sequence_on G holds
f :- p is_sequence_on G
let p be Element of D; :: thesis: ( p in rng f & f is_sequence_on G implies f :- p is_sequence_on G )
assume that
A1: p in rng f and
A2: f is_sequence_on G ; :: thesis: f :- p is_sequence_on G
ex i being Element of NAT st
( i + 1 = p .. f & f :- p = f /^ i ) by A1, FINSEQ_5:49;
hence f :- p is_sequence_on G by A2, JORDAN8:2; :: thesis: verum