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