let p be FinSequence; :: thesis: for x, y being object holds
( p = <*x,y*> iff ( len p = 2 & p . 1 = x & p . 2 = y ) )
let x, y be object ; :: thesis: ( p = <*x,y*> iff ( len p = 2 & p . 1 = x & p . 2 = y ) )
thus ( p = <*x,y*> implies ( len p = 2 & p . 1 = x & p . 2 = y ) ) :: thesis: ( len p = 2 & p . 1 = x & p . 2 = y implies p = <*x,y*> )

proof

assume A1: p = <*x,y*> ; :: thesis: ( len p = 2 & p . 1 = x & p . 2 = y )
hence len p = (len <*x*>) + (len <*y*>) by Th22
.= 1 + (len <*y*>) by Th39
.= 1 + 1 by Th39
.= 2 ;
:: thesis: ( p . 1 = x & p . 2 = y )
A2: 1 in {1} by TARSKI:def 1;
then 1 in dom <*x*> by Def8, Th2;
hence p . 1 = <*x*> . 1 by A1, Def7
.= x ;
:: thesis: p . 2 = y
A3: 1 in dom <*y*> by A2, Def8, Th2;
thus p . 2 = (<*x*> ^ <*y*>) . (1 + 1) by A1
.= (<*x*> ^ <*y*>) . ((len <*x*>) + 1) by Th39
.= <*y*> . 1 by A3, Def7
.= y ; :: thesis: verum

end;

assume that
A4: len p = 2 and
A5: p . 1 = x and
A6: p . 2 = y ; :: thesis: p = <*x,y*>
A7: dom p = Seg (1 + 1) by A4, Def3
.= Seg ((len <*x*>) + 1) by Th39
.= Seg ((len <*x*>) + (len <*y*>)) by Th39 ;
A8: for k being Nat st k in dom <*x*> holds
p . k = <*x*> . k

proof

let k be Nat; :: thesis: ( k in dom <*x*> implies p . k = <*x*> . k )
assume k in dom <*x*> ; :: thesis: p . k = <*x*> . k
then k in {1} by Def8, Th2;
then k = 1 by TARSKI:def 1;
hence p . k = <*x*> . k by A5; :: thesis: verum

end;

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

proof

let k be Nat; :: thesis: ( k in dom <*y*> implies p . ((len <*x*>) + k) = <*y*> . k )
assume k in dom <*y*> ; :: thesis: p . ((len <*x*>) + k) = <*y*> . k
then A9: k in {1} by Def8, Th2;
thus p . ((len <*x*>) + k) = p . (1 + k) by Th39
.= p . (1 + 1) by A9, TARSKI:def 1
.= <*y*> . 1 by A6
.= <*y*> . k by A9, TARSKI:def 1 ; :: thesis: verum

end;

hence p = <*x,y*> by A7, A8, Def7; :: thesis: verum