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

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