let D be non empty set ; :: thesis: for f being FinSequence of D
for G being Matrix of D
for p being set st 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 set st f is_sequence_on G holds
f -: p is_sequence_on G
let G be Matrix of D; :: thesis: for p being set st f is_sequence_on G holds
f -: p is_sequence_on G
let p be set ; :: thesis: ( f is_sequence_on G implies f -: p is_sequence_on G )
assume f is_sequence_on G ; :: thesis: f -: p is_sequence_on G
then f | (p .. f) is_sequence_on G by GOBOARD1:22;
hence f -: p is_sequence_on G by FINSEQ_5:def 1; :: thesis: verum