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 /^ 2 = <*c*>

let D be non empty set ; :: thesis: for f being FinSequence of D st f = <*a,b,c*> holds

f /^ 2 = <*c*>

let f be FinSequence of D; :: thesis: ( f = <*a,b,c*> implies f /^ 2 = <*c*> )

assume A1: f = <*a,b,c*> ; :: thesis: f /^ 2 = <*c*>

then reconsider a2 = a, b2 = b, c2 = c as Element of D by Th10;

f /^ 2 = (<*a2*> ^ <*b2,c2*>) /^ (1 + 1) by A1, FINSEQ_1:43

.= (<*a2*> ^ <*b2,c2*>) /^ ((len <*a2*>) + 1) by FINSEQ_1:40

.= <*b2,c2*> /^ 1 by FINSEQ_5:36

.= <*c2*> by FINSEQ_6:46 ;

hence f /^ 2 = <*c*> ; :: thesis: verum

for f being FinSequence of D st f = <*a,b,c*> holds

f /^ 2 = <*c*>

let D be non empty set ; :: thesis: for f being FinSequence of D st f = <*a,b,c*> holds

f /^ 2 = <*c*>

let f be FinSequence of D; :: thesis: ( f = <*a,b,c*> implies f /^ 2 = <*c*> )

assume A1: f = <*a,b,c*> ; :: thesis: f /^ 2 = <*c*>

then reconsider a2 = a, b2 = b, c2 = c as Element of D by Th10;

f /^ 2 = (<*a2*> ^ <*b2,c2*>) /^ (1 + 1) by A1, FINSEQ_1:43

.= (<*a2*> ^ <*b2,c2*>) /^ ((len <*a2*>) + 1) by FINSEQ_1:40

.= <*b2,c2*> /^ 1 by FINSEQ_5:36

.= <*c2*> by FINSEQ_6:46 ;

hence f /^ 2 = <*c*> ; :: thesis: verum