let x1, x2, x3, x4, x5 be set ; :: thesis: for p being FinSequence holds
( p = <*x1,x2,x3,x4,x5*> iff ( len p = 5 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 ) )
let p be FinSequence; :: thesis: ( p = <*x1,x2,x3,x4,x5*> iff ( len p = 5 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 ) )
thus
( p = <*x1,x2,x3,x4,x5*> implies ( len p = 5 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 ) )
:: thesis: ( len p = 5 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 implies p = <*x1,x2,x3,x4,x5*> )proof
assume A1:
p = <*x1,x2,x3,x4,x5*>
;
:: thesis: ( len p = 5 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 )
hence len p =
len (<*x1,x2,x3,x4*> ^ <*x5*>)
by Th90
.=
(len <*x1,x2,x3,x4*>) + (len <*x5*>)
by FINSEQ_1:35
.=
4
+ (len <*x5*>)
by Th91
.=
4
+ 1
by FINSEQ_1:57
.=
5
;
:: thesis: ( p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 )
set p4 =
<*x1,x2,x3,x4*>;
A2:
dom <*x1,x2,x3,x4*> = {1,2,3,4}
by Th92, FINSEQ_3:2;
A3:
p = <*x1,x2,x3,x4*> ^ <*x5*>
by A1, Th90;
1
in dom <*x1,x2,x3,x4*>
by A2, ENUMSET1:def 2;
hence p . 1 =
<*x1,x2,x3,x4*> . 1
by A3, FINSEQ_1:def 7
.=
x1
by Th91
;
:: thesis: ( p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 )
2
in dom <*x1,x2,x3,x4*>
by A2, ENUMSET1:def 2;
hence p . 2 =
<*x1,x2,x3,x4*> . 2
by A3, FINSEQ_1:def 7
.=
x2
by Th91
;
:: thesis: ( p . 3 = x3 & p . 4 = x4 & p . 5 = x5 )
3
in dom <*x1,x2,x3,x4*>
by A2, ENUMSET1:def 2;
hence p . 3 =
<*x1,x2,x3,x4*> . 3
by A3, FINSEQ_1:def 7
.=
x3
by Th91
;
:: thesis: ( p . 4 = x4 & p . 5 = x5 )
4
in dom <*x1,x2,x3,x4*>
by A2, ENUMSET1:def 2;
hence p . 4 =
<*x1,x2,x3,x4*> . 4
by A3, FINSEQ_1:def 7
.=
x4
by Th91
;
:: thesis: p . 5 = x5
1
in {1}
by TARSKI:def 1;
then A4:
1
in dom <*x5*>
by FINSEQ_1:4, FINSEQ_1:def 8;
thus p . 5 =
(<*x1,x2,x3,x4*> ^ <*x5*>) . (4 + 1)
by A1, Th90
.=
(<*x1,x2,x3,x4*> ^ <*x5*>) . ((len <*x1,x2,x3,x4*>) + 1)
by Th91
.=
<*x5*> . 1
by A4, FINSEQ_1:def 7
.=
x5
by FINSEQ_1:def 8
;
:: thesis: verum
end;
assume A5:
( len p = 5 & p . 1 = x1 & p . 2 = x2 & p . 3 = x3 & p . 4 = x4 & p . 5 = x5 )
; :: thesis: p = <*x1,x2,x3,x4,x5*>
set p4 = <*x1,x2,x3,x4*>;
A6: dom p =
Seg (4 + 1)
by A5, FINSEQ_1:def 3
.=
Seg ((len <*x1,x2,x3,x4*>) + 1)
by Th91
.=
Seg ((len <*x1,x2,x3,x4*>) + (len <*x5*>))
by FINSEQ_1:56
;
A7:
for k being Nat st k in dom <*x1,x2,x3,x4*> holds
p . k = <*x1,x2,x3,x4*> . k
proof
let k be
Nat;
:: thesis: ( k in dom <*x1,x2,x3,x4*> implies p . k = <*x1,x2,x3,x4*> . k )
assume A8:
k in dom <*x1,x2,x3,x4*>
;
:: thesis: p . k = <*x1,x2,x3,x4*> . k
len <*x1,x2,x3,x4*> = 4
by Th91;
then A9:
k in {1,2,3,4}
by A8, FINSEQ_1:def 3, FINSEQ_3:2;
end;
for k being Nat st k in dom <*x5*> holds
p . ((len <*x1,x2,x3,x4*>) + k) = <*x5*> . k
proof
let k be
Nat;
:: thesis: ( k in dom <*x5*> implies p . ((len <*x1,x2,x3,x4*>) + k) = <*x5*> . k )
assume
k in dom <*x5*>
;
:: thesis: p . ((len <*x1,x2,x3,x4*>) + k) = <*x5*> . k
then
k in {1}
by FINSEQ_1:4, FINSEQ_1:def 8;
then A10:
k = 1
by TARSKI:def 1;
hence p . ((len <*x1,x2,x3,x4*>) + k) =
p . (4 + 1)
by Th91
.=
<*x5*> . k
by A5, A10, FINSEQ_1:def 8
;
:: thesis: verum
end;
hence p =
<*x1,x2,x3,x4*> ^ <*x5*>
by A6, A7, FINSEQ_1:def 7
.=
<*x1,x2,x3,x4,x5*>
by Th90
;
:: thesis: verum