let p be FinSequence; for x, y, z being object holds
( p = <*x,y,z*> iff ( len p = 3 & p . 1 = x & p . 2 = y & p . 3 = z ) )
let x, y, z be object ; ( p = <*x,y,z*> iff ( len p = 3 & p . 1 = x & p . 2 = y & p . 3 = z ) )
thus
( p = <*x,y,z*> implies ( len p = 3 & p . 1 = x & p . 2 = y & p . 3 = z ) )
( len p = 3 & p . 1 = x & p . 2 = y & p . 3 = z implies p = <*x,y,z*> )proof
assume A1:
p = <*x,y,z*>
;
( len p = 3 & p . 1 = x & p . 2 = y & p . 3 = z )
hence len p =
(len <*x,y*>) + (len <*z*>)
by Th22
.=
2
+ (len <*z*>)
by Th44
.=
2
+ 1
by Th39
.=
3
;
( p . 1 = x & p . 2 = y & p . 3 = z )
A2:
1
in {1}
by TARSKI:def 1;
then A3:
1
in dom <*x*>
by Def8, Th2;
thus p . 1 =
(<*x*> ^ <*y,z*>) . 1
by A1, Th32
.=
<*x*> . 1
by A3, Def7
.=
x
by Def8
;
( p . 2 = y & p . 3 = z )
( 2
in Seg 2 &
len <*x,y*> = 2 )
by Th44;
then
2
in dom <*x,y*>
by Def3;
hence p . 2 =
<*x,y*> . 2
by A1, Def7
.=
y
by Th44
;
p . 3 = z
A4:
1
in dom <*z*>
by A2, Def8, Th2;
thus p . 3 =
(<*x,y*> ^ <*z*>) . (2 + 1)
by A1
.=
(<*x,y*> ^ <*z*>) . ((len <*x,y*>) + 1)
by Th44
.=
<*z*> . 1
by A4, Def7
.=
z
by Def8
;
verum
end;
assume that
A5:
len p = 3
and
A6:
p . 1 = x
and
A7:
p . 2 = y
and
A8:
p . 3 = z
; p = <*x,y,z*>
A9: dom p =
Seg (2 + 1)
by A5, Def3
.=
Seg ((len <*x,y*>) + 1)
by Th44
.=
Seg ((len <*x,y*>) + (len <*z*>))
by Th39
;
A10:
for k being Nat st k in dom <*x,y*> holds
p . k = <*x,y*> . k
proof
let k be
Nat;
( k in dom <*x,y*> implies p . k = <*x,y*> . k )
assume A11:
k in dom <*x,y*>
;
p . k = <*x,y*> . k
len <*x,y*> = 2
by Th44;
then A12:
k in Seg 2
by A11, Def3;
A13:
(
k = 1 implies
p . k = <*x,y*> . k )
by A6, Th44;
(
k = 2 implies
p . k = <*x,y*> . k )
by A7, Th44;
hence
p . k = <*x,y*> . k
by A12, A13, Th2, TARSKI:def 2;
verum
end;
for k being Nat st k in dom <*z*> holds
p . ((len <*x,y*>) + k) = <*z*> . k
hence
p = <*x,y,z*>
by A9, A10, Def7; verum