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, FINSEQ_1:45;

( f . 1 = a2 & f . 2 = b2 ) by A1, FINSEQ_1:45;

hence f /^ 1 = <*b,c*> by A1, A2, FINSEQ_6:47; :: thesis: verum

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, FINSEQ_1:45;

( f . 1 = a2 & f . 2 = b2 ) by A1, FINSEQ_1:45;

hence f /^ 1 = <*b,c*> by A1, A2, FINSEQ_6:47; :: thesis: verum