let a1, a2, a3, a4, a5, a6, a7, a8, a9, a10 be object ; 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; ( 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 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;
( 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*>
;
( 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
;
( 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 )
;
f . 10 = a10
len <*a1,a2,a3,a4,a5,a6,a7,a8,a9*> = 9
by Th1;
hence
f . 10
= a10
by A2;
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 ) )
; ( 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
; ( 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 )
; f = <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*>
now for x being object st x in Seg 10 holds
f . x = <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> . xlet x be
object ;
( x in Seg 10 implies f . x = <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> . x )assume
x in Seg 10
;
f . x = <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*> . xthen
(
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;
verum end;
hence
f = <*a1,a2,a3,a4,a5,a6,a7,a8,a9,a10*>
by A4, FUNCT_1:2; verum