let a1, a2, a3, a4, a5, a6 be object ; :: thesis: for f being FinSequence holds
( f = <*a1,a2,a3,a4,a5,a6*> iff ( len f = 6 & f . 1 = a1 & f . 2 = a2 & f . 3 = a3 & f . 4 = a4 & f . 5 = a5 & f . 6 = a6 ) )
let f be FinSequence; :: thesis: ( f = <*a1,a2,a3,a4,a5,a6*> iff ( len f = 6 & f . 1 = a1 & f . 2 = a2 & f . 3 = a3 & f . 4 = a4 & f . 5 = a5 & f . 6 = a6 ) )

A1: now :: thesis: for f being FinSequence st f = <*a1,a2,a3,a4,a5,a6*> holds
( len f = 6 & f . 1 = a1 & f . 2 = a2 & f . 3 = a3 & f . 4 = a4 & f . 5 = a5 & f . 6 = a6 )

let f be FinSequence; :: thesis: ( f = <*a1,a2,a3,a4,a5,a6*> implies ( len f = 6 & f . 1 = a1 & f . 2 = a2 & f . 3 = a3 & f . 4 = a4 & f . 5 = a5 & f . 6 = a6 ) )
assume A2: f = <*a1,a2,a3,a4,a5,a6*> ; :: thesis: ( len f = 6 & f . 1 = a1 & f . 2 = a2 & f . 3 = a3 & f . 4 = a4 & f . 5 = a5 & f . 6 = a6 )
hence len f = (len <*a1,a2,a3,a4,a5*>) + (len <*a6*>) by FINSEQ_1:22
.= 5 + (len <*a6*>) by FINSEQ_4:78
.= 5 + 1 by FINSEQ_1:39
.= 6 ;
:: thesis: ( f . 1 = a1 & f . 2 = a2 & f . 3 = a3 & f . 4 = a4 & f . 5 = a5 & f . 6 = a6 )
dom <*a1,a2,a3,a4,a5*> = Seg 5 by FINSEQ_1:89;
then ( 1 in dom <*a1,a2,a3,a4,a5*> & 2 in dom <*a1,a2,a3,a4,a5*> & 3 in dom <*a1,a2,a3,a4,a5*> & 4 in dom <*a1,a2,a3,a4,a5*> & 5 in dom <*a1,a2,a3,a4,a5*> ) ;
then ( f . 1 = <*a1,a2,a3,a4,a5*> . 1 & f . 2 = <*a1,a2,a3,a4,a5*> . 2 & f . 3 = <*a1,a2,a3,a4,a5*> . 3 & f . 4 = <*a1,a2,a3,a4,a5*> . 4 & f . 5 = <*a1,a2,a3,a4,a5*> . 5 ) by A2, FINSEQ_1:def 7;
hence ( f . 1 = a1 & f . 2 = a2 & f . 3 = a3 & f . 4 = a4 & f . 5 = a5 ) ; :: thesis: f . 6 = a6
A3: len <*a1,a2,a3,a4,a5*> = 5 by FINSEQ_4:78;
1 in Seg 1 ;
then ( 1 in dom <*a6*> & 5 + 1 = 6 ) by FINSEQ_1:89;
hence f . 6 = <*a6*> . 1 by A2, A3, FINSEQ_1:def 7
.= a6 ;
:: thesis: verum

end;

hence ( f = <*a1,a2,a3,a4,a5,a6*> implies ( len f = 6 & f . 1 = a1 & f . 2 = a2 & f . 3 = a3 & f . 4 = a4 & f . 5 = a5 & f . 6 = a6 ) ) ; :: thesis: ( len f = 6 & f . 1 = a1 & f . 2 = a2 & f . 3 = a3 & f . 4 = a4 & f . 5 = a5 & f . 6 = a6 implies f = <*a1,a2,a3,a4,a5,a6*> )
assume A4: len f = 6 ; :: thesis: ( not f . 1 = a1 or not f . 2 = a2 or not f . 3 = a3 or not f . 4 = a4 or not f . 5 = a5 or not f . 6 = a6 or f = <*a1,a2,a3,a4,a5,a6*> )
len <*a1,a2,a3,a4,a5,a6*> = 6 by A1;
then A5: ( dom f = Seg 6 & dom <*a1,a2,a3,a4,a5,a6*> = Seg 6 ) by A4, FINSEQ_1:def 3;
assume A6: f . 1 = a1 ; :: thesis: ( not f . 2 = a2 or not f . 3 = a3 or not f . 4 = a4 or not f . 5 = a5 or not f . 6 = a6 or f = <*a1,a2,a3,a4,a5,a6*> )
assume A7: f . 2 = a2 ; :: thesis: ( not f . 3 = a3 or not f . 4 = a4 or not f . 5 = a5 or not f . 6 = a6 or f = <*a1,a2,a3,a4,a5,a6*> )
assume A8: f . 3 = a3 ; :: thesis: ( not f . 4 = a4 or not f . 5 = a5 or not f . 6 = a6 or f = <*a1,a2,a3,a4,a5,a6*> )
assume A9: f . 4 = a4 ; :: thesis: ( not f . 5 = a5 or not f . 6 = a6 or f = <*a1,a2,a3,a4,a5,a6*> )
assume A10: f . 5 = a5 ; :: thesis: ( not f . 6 = a6 or f = <*a1,a2,a3,a4,a5,a6*> )
assume A11: f . 6 = a6 ; :: thesis: f = <*a1,a2,a3,a4,a5,a6*>

now :: thesis: for x being object st x in Seg 6 holds
f . x = <*a1,a2,a3,a4,a5,a6*> . x

let x be object ; :: thesis: ( x in Seg 6 implies f . x = <*a1,a2,a3,a4,a5,a6*> . x )
assume x in Seg 6 ; :: thesis: f . x = <*a1,a2,a3,a4,a5,a6*> . x
then ( x = 1 or x = 2 or x = 3 or x = 4 or x = 5 or x = 6 ) by FINSEQ_3:4, ENUMSET1:def 4;
hence f . x = <*a1,a2,a3,a4,a5,a6*> . x by A1, A6, A7, A8, A9, A10, A11; :: thesis: verum

end;

hence f = <*a1,a2,a3,a4,a5,a6*> by A5; :: thesis: verum