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