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

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

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

end;

hence ( f = <*a1,a2,a3,a4,a5,a6,a7,a8*> implies ( len f = 8 & f . 1 = a1 & f . 2 = a2 & f . 3 = a3 & f . 4 = a4 & f . 5 = a5 & f . 6 = a6 & f . 7 = a7 & f . 8 = a8 ) ) ; :: thesis: ( len f = 8 & f . 1 = a1 & f . 2 = a2 & f . 3 = a3 & f . 4 = a4 & f . 5 = a5 & f . 6 = a6 & f . 7 = a7 & f . 8 = a8 implies f = <*a1,a2,a3,a4,a5,a6,a7,a8*> )
assume A5: len f = 8 ; :: 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 not f . 7 = a7 or not f . 8 = a8 or f = <*a1,a2,a3,a4,a5,a6,a7,a8*> )
len <*a1,a2,a3,a4,a5,a6,a7,a8*> = 8 by A1;
then A6: ( dom f = Seg 8 & dom <*a1,a2,a3,a4,a5,a6,a7,a8*> = Seg 8 ) by A5, FINSEQ_1:def 3;
assume A7: 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 not f . 7 = a7 or not f . 8 = a8 or f = <*a1,a2,a3,a4,a5,a6,a7,a8*> )
assume A8: f . 2 = a2 ; :: thesis: ( not f . 3 = a3 or not f . 4 = a4 or not f . 5 = a5 or not f . 6 = a6 or not f . 7 = a7 or not f . 8 = a8 or f = <*a1,a2,a3,a4,a5,a6,a7,a8*> )
assume A9: f . 3 = a3 ; :: thesis: ( not f . 4 = a4 or not f . 5 = a5 or not f . 6 = a6 or not f . 7 = a7 or not f . 8 = a8 or f = <*a1,a2,a3,a4,a5,a6,a7,a8*> )
assume A10: f . 4 = a4 ; :: thesis: ( not f . 5 = a5 or not f . 6 = a6 or not f . 7 = a7 or not f . 8 = a8 or f = <*a1,a2,a3,a4,a5,a6,a7,a8*> )
assume A11: f . 5 = a5 ; :: thesis: ( not f . 6 = a6 or not f . 7 = a7 or not f . 8 = a8 or f = <*a1,a2,a3,a4,a5,a6,a7,a8*> )
assume A12: f . 6 = a6 ; :: thesis: ( not f . 7 = a7 or not f . 8 = a8 or f = <*a1,a2,a3,a4,a5,a6,a7,a8*> )
assume A13: f . 7 = a7 ; :: thesis: ( not f . 8 = a8 or f = <*a1,a2,a3,a4,a5,a6,a7,a8*> )
assume A14: f . 8 = a8 ; :: thesis: f = <*a1,a2,a3,a4,a5,a6,a7,a8*>

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

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

end;

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