let x1, x2, x3, x4 be object ; for p being FinSequence holds
( p = <*x1,x2,x3,x4*> iff ( len p = 4 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 ) )
let p be FinSequence; ( p = <*x1,x2,x3,x4*> iff ( len p = 4 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 ) )
thus
( p = <*x1,x2,x3,x4*> implies ( len p = 4 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 ) )
( len p = 4 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 implies p = <*x1,x2,x3,x4*> )proof
set p3 =
<*x1,x2,x3*>;
assume A1:
p = <*x1,x2,x3,x4*>
;
( len p = 4 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 )
hence len p =
(len <*x1,x2,x3*>) + (len <*x4*>)
by FINSEQ_1:22
.=
3
+ (len <*x4*>)
by FINSEQ_1:45
.=
3
+ 1
by FINSEQ_1:40
.=
4
;
( p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 )
A2:
dom <*x1,x2,x3*> = {1,2,3}
by FINSEQ_1:89, FINSEQ_3:1;
then
1
in dom <*x1,x2,x3*>
by ENUMSET1:def 1;
hence p . 1 =
<*x1,x2,x3*> . 1
by A1, FINSEQ_1:def 7
.=
x1
by FINSEQ_1:45
;
( p . 2 = x2 & p . 3 = x3 & p . 4 = x4 )
2
in dom <*x1,x2,x3*>
by A2, ENUMSET1:def 1;
hence p . 2 =
<*x1,x2,x3*> . 2
by A1, FINSEQ_1:def 7
.=
x2
by FINSEQ_1:45
;
( p . 3 = x3 & p . 4 = x4 )
3
in dom <*x1,x2,x3*>
by A2, ENUMSET1:def 1;
hence p . 3 =
<*x1,x2,x3*> . 3
by A1, FINSEQ_1:def 7
.=
x3
by FINSEQ_1:45
;
p . 4 = x4
1
in {1}
by TARSKI:def 1;
then A3:
1
in dom <*x4*>
by FINSEQ_1:2, FINSEQ_1:def 8;
thus p . 4 =
(<*x1,x2,x3*> ^ <*x4*>) . (3 + 1)
by A1
.=
(<*x1,x2,x3*> ^ <*x4*>) . ((len <*x1,x2,x3*>) + 1)
by FINSEQ_1:45
.=
<*x4*> . 1
by A3, FINSEQ_1:def 7
.=
x4
by FINSEQ_1:def 8
;
verum
end;
assume that
A4:
len p = 4
and
A5:
p . 1 = x1
and
A6:
p . 2 = x2
and
A7:
p . 3 = x3
and
A8:
p . 4 = x4
; p = <*x1,x2,x3,x4*>
A9:
for k being Nat st k in dom <*x1,x2,x3*> holds
p . k = <*x1,x2,x3*> . k
proof
A10:
len <*x1,x2,x3*> = 3
by FINSEQ_1:45;
let k be
Nat;
( k in dom <*x1,x2,x3*> implies p . k = <*x1,x2,x3*> . k )
assume
k in dom <*x1,x2,x3*>
;
p . k = <*x1,x2,x3*> . k
then A11:
k in {1,2,3}
by A10, FINSEQ_1:def 3, FINSEQ_3:1;
end;
A12:
for k being Nat st k in dom <*x4*> holds
p . ((len <*x1,x2,x3*>) + k) = <*x4*> . k
dom p =
Seg (3 + 1)
by A4, FINSEQ_1:def 3
.=
Seg ((len <*x1,x2,x3*>) + 1)
by FINSEQ_1:45
.=
Seg ((len <*x1,x2,x3*>) + (len <*x4*>))
by FINSEQ_1:39
;
hence
p = <*x1,x2,x3,x4*>
by A9, A12, FINSEQ_1:def 7; verum