let p be FinSequence; :: thesis: 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 ; :: thesis: ( 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 ) ) :: thesis: ( len p = 3 & p . 1 = x & p . 2 = y & p . 3 = z implies p = <*x,y,z*> )

proof

assume A1: p = <*x,y,z*> ; :: thesis: ( 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 ;
:: thesis: ( 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 ; :: thesis: ( 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 ;
:: thesis: 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 ; :: thesis: verum

end;

assume that
A5: len p = 3 and
A6: p . 1 = x and
A7: p . 2 = y and
A8: p . 3 = z ; :: thesis: 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; :: thesis: ( k in dom <*x,y*> implies p . k = <*x,y*> . k )
assume A11: k in dom <*x,y*> ; :: thesis: 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;
( k = 2 implies p . k = <*x,y*> . k ) by A7;
hence p . k = <*x,y*> . k by A12, A13, Th2, TARSKI:def 2; :: thesis: verum

end;

for k being Nat st k in dom <*z*> holds
p . ((len <*x,y*>) + k) = <*z*> . k

proof

let k be Nat; :: thesis: ( k in dom <*z*> implies p . ((len <*x,y*>) + k) = <*z*> . k )
assume k in dom <*z*> ; :: thesis: p . ((len <*x,y*>) + k) = <*z*> . k
then k in {1} by Def8, Th2;
then A14: k = 1 by TARSKI:def 1;
hence p . ((len <*x,y*>) + k) = p . (2 + 1) by Th44
.= <*z*> . k by A8, A14 ;
:: thesis: verum

end;

hence p = <*x,y,z*> by A9, A10, Def7; :: thesis: verum