let a, b, c be set ; :: thesis: for D being non empty set
for f being FinSequence of D st f = <*a,b,c*> holds
f /^ 1 = <*b,c*>
let D be non empty set ; :: thesis: for f being FinSequence of D st f = <*a,b,c*> holds
f /^ 1 = <*b,c*>
let f be FinSequence of D; :: thesis: ( f = <*a,b,c*> implies f /^ 1 = <*b,c*> )
assume A1: f = <*a,b,c*> ; :: thesis: f /^ 1 = <*b,c*>
then reconsider a2 = a, b2 = b, c2 = c as Element of D by Th10;
A2: f . 3 = c2 by A1;
( f . 1 = a2 & f . 2 = b2 ) by A1;
hence f /^ 1 = <*b,c*> by A1, A2, FINSEQ_6:47; :: thesis: verum