let x, y, z be object ; :: thesis: for p being XFinSequence holds
( p = <%x,y,z%> iff ( len p = 3 & p . 0 = x & p . 1 = y & p . 2 = z ) )
let p be XFinSequence; :: thesis: ( p = <%x,y,z%> iff ( len p = 3 & p . 0 = x & p . 1 = y & p . 2 = z ) )
thus ( p = <%x,y,z%> implies ( len p = 3 & p . 0 = x & p . 1 = y & p . 2 = z ) ) :: thesis: ( len p = 3 & p . 0 = x & p . 1 = y & p . 2 = z implies p = <%x,y,z%> )

proof

A2: 0 in dom <%x%> by TARSKI:def 1;
A3: 0 in dom <%z%> by TARSKI:def 1;
assume A4: p = <%x,y,z%> ; :: thesis: ( len p = 3 & p . 0 = x & p . 1 = y & p . 2 = z )
hence len p = (len <%x,y%>) + (len <%z%>) by Def3
.= 2 + (len <%z%>) by Th35
.= 2 + 1 by Th30
.= 3 ;
:: thesis: ( p . 0 = x & p . 1 = y & p . 2 = z )
thus p . 0 = (<%x%> ^ <%y,z%>) . 0 by A4, Th25
.= <%x%> . 0 by A2, Def3
.= x ; :: thesis: ( p . 1 = y & p . 2 = z )
( 1 in Segm (1 + 1) & len <%x,y%> = 2 ) by Th35, NAT_1:45;
hence p . 1 = <%x,y%> . 1 by A4, Def3
.= y ;
:: thesis: p . 2 = z
thus p . 2 = (<%x,y%> ^ <%z%>) . ((len <%x,y%>) + 0) by A4, Th35
.= <%z%> . 0 by A3, Def3
.= z ; :: thesis: verum

end;

assume that
A5: len p = 3 and
A6: p . 0 = x and
A7: p . 1 = y and
A8: p . 2 = z ; :: thesis: p = <%x,y,z%>
A9: for k being Nat st k in dom <%x,y%> holds
p . k = <%x,y%> . k

proof

A10: len <%x,y%> = 2 by Th35;
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
A12: ( k = 1 implies p . k = <%x,y%> . k ) by A7;
( k = 0 implies p . k = <%x,y%> . k ) by A6;
hence p . k = <%x,y%> . k by A11, A10, A12, CARD_1:50, TARSKI:def 2; :: thesis: verum

end;

A13: 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 A14: k = 0 by TARSKI:def 1;
hence p . ((len <%x,y%>) + k) = p . (2 + 0) by Th35
.= <%z%> . k by A8, A14 ;
:: thesis: verum

end;

dom p = 2 + 1 by A5
.= (len <%x,y%>) + 1 by Th35
.= (len <%x,y%>) + (len <%z%>) by Th30 ;
hence p = <%x,y,z%> by A9, A13, Def3; :: thesis: verum