let x, y, z be set ; :: 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

assume A1: 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 Def4
.= 2 + (len <%z%>) by Th42
.= 2 + 1 by Th36
.= 3 ;
:: thesis: ( p . 0 = x & p . 1 = y & p . 2 = z )
A2: 0 in {0 } by TARSKI:def 1;
then A3: 0 in dom <%x%> by Def5, CARD_1:87;
thus p . 0 = (<%x%> ^ <%y,z%>) . 0 by A1, Th30
.= <%x%> . 0 by A3, Def4
.= x by Def5 ; :: thesis: ( p . 1 = y & p . 2 = z )
A4: 1 in 1 + 1 by Th1;
len <%x,y%> = 2 by Th42;
hence p . 1 = <%x,y%> . 1 by A1, A4, Def4
.= y by Th42 ;
:: thesis: p . 2 = z
A5: 0 in dom <%z%> by A2, Def5, CARD_1:87;
thus p . 2 = (<%x,y%> ^ <%z%>) . ((len <%x,y%>) + 0 ) by A1, Th42
.= <%z%> . 0 by A5, Def4
.= z by Def5 ; :: thesis: verum

end;

assume A6: ( len p = 3 & p . 0 = x & p . 1 = y & p . 2 = z ) ; :: thesis: p = <%x,y,z%>
then A7: dom p = 2 + 1
.= (len <%x,y%>) + 1 by Th42
.= (len <%x,y%>) + (len <%z%>) by Th36 ;
A8: for k being Element of NAT st k in dom <%x,y%> holds
p . k = <%x,y%> . k

proof

let k be Element of NAT ; :: thesis: ( k in dom <%x,y%> implies p . k = <%x,y%> . k )
assume A9: k in dom <%x,y%> ; :: thesis: p . k = <%x,y%> . k
B10: len <%x,y%> = 2 by Th42;
A11: ( k = 0 implies p . k = <%x,y%> . k ) by A6, Th42;
( k = 1 implies p . k = <%x,y%> . k ) by A6, Th42;
hence p . k = <%x,y%> . k by A9, B10, A11, CARD_1:88, TARSKI:def 2; :: thesis: verum

end;

for k being Element of NAT st k in dom <%z%> holds
p . ((len <%x,y%>) + k) = <%z%> . k

proof

let k be Element of 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 {0 } by Def5, CARD_1:87;
then A12: k = 0 by TARSKI:def 1;
hence p . ((len <%x,y%>) + k) = p . (2 + 0 ) by Th42
.= <%z%> . k by A6, A12, Def5 ;
:: thesis: verum

end;

hence p = <%x,y,z%> by A7, A8, Def4; :: thesis: verum