let a1, a2, a3, a4, a5, a6, a7, a8, a9, a10 be object ; :: thesis: for f being FinSequence holds
( f = <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> iff ( len f = 10 & 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 & f . 10 = a10 ) )
let f be FinSequence; :: thesis: ( f = <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> iff ( len f = 10 & 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 & f . 10 = a10 ) )
set AS1 = <*a10*>;
set AS9 = <*a1,a2,a3,a4,a5,a6,a7,a8,a9*>;
set AS10 = <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*>;

A1: now :: thesis: for f being FinSequence st f = <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> holds
( len f = 10 & 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 & f . 10 = a10 )

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

end;

hence ( f = <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> implies ( len f = 10 & 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 & f . 10 = a10 ) ) ; :: thesis: ( len f = 10 & 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 & f . 10 = a10 implies f = <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> )
assume A3: len f = 10 ; :: 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 not f . 10 = a10 or f = <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> )
len <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> = 10 by A1;
then A4: ( dom f = Seg 10 & dom <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> = Seg 10 ) 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 & f . 10 = a10 ) ; :: thesis: f = <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*>

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

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

end;

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