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

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

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

end;

hence ( f = <*a1,a2,a3,a4,a5,a6,a7,a8,a9*> implies ( len f = 9 & f . 1 = a1 & f . 2 = a2 & f . 3 = a3 & f . 4 = a4 & f . 5 = a5 & f . 6 = a6 & f . 7 = a7 & f . 8 = a8 & f . 9 = a9 ) ) ; :: thesis: ( len f = 9 & f . 1 = a1 & f . 2 = a2 & f . 3 = a3 & f . 4 = a4 & f . 5 = a5 & f . 6 = a6 & f . 7 = a7 & f . 8 = a8 & f . 9 = a9 implies f = <*a1,a2,a3,a4,a5,a6,a7,a8,a9*> )
assume A3: len f = 9 ; :: 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 not f . 9 = a9 or f = <*a1,a2,a3,a4,a5,a6,a7,a8,a9*> )
len <*a1,a2,a3,a4,a5,a6,a7,a8,a9*> = 9 by A1;
then A4: ( dom f = Seg 9 & dom <*a1,a2,a3,a4,a5,a6,a7,a8,a9*> = Seg 9 ) by A3, FINSEQ_1:def 3;
assume A5: ( f . 1 = a1 & f . 2 = a2 & f . 3 = a3 & f . 4 = a4 & f . 5 = a5 & f . 6 = a6 & f . 7 = a7 & f . 8 = a8 & f . 9 = a9 ) ; :: thesis: f = <*a1,a2,a3,a4,a5,a6,a7,a8,a9*>

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

let x be object ; :: thesis: ( x in Seg 9 implies f . x = <*a1,a2,a3,a4,a5,a6,a7,a8,a9*> . x )
assume x in Seg 9 ; :: thesis: f . x = <*a1,a2,a3,a4,a5,a6,a7,a8,a9*> . 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 or x = 9 ) by AOFA_A00:27, ENUMSET1:def 7;
hence f . x = <*a1,a2,a3,a4,a5,a6,a7,a8,a9*> . x by A1, A5; :: thesis: verum

end;

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