let a1, a2, a3, a4, a5, a6, a7, a8 be object ; 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; ( 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 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;
( 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*>
;
( 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
;
( 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 )
by FINSEQ_4:78;
( 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
by FINSEQ_1:45
;
( 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
by FINSEQ_1:45
;
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
by FINSEQ_1:45
;
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 ) )
; ( 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
; ( 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
; ( 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
; ( 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
; ( 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
; ( 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
; ( 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
; ( not f . 7 = a7 or not f . 8 = a8 or f = <*a1,a2,a3,a4,a5,a6,a7,a8*> )
assume A13:
f . 7 = a7
; ( not f . 8 = a8 or f = <*a1,a2,a3,a4,a5,a6,a7,a8*> )
assume A14:
f . 8 = a8
; f = <*a1,a2,a3,a4,a5,a6,a7,a8*>
now for x being object st x in Seg 8 holds
f . x = <*a1,a2,a3,a4,a5,a6,a7,a8*> . xlet x be
object ;
( x in Seg 8 implies f . x = <*a1,a2,a3,a4,a5,a6,a7,a8*> . x )assume
x in Seg 8
;
f . x = <*a1,a2,a3,a4,a5,a6,a7,a8*> . xthen
(
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;
verum end;
hence
f = <*a1,a2,a3,a4,a5,a6,a7,a8*>
by A6; verum