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

proof

assume A1: p = <%x,y%> ; :: thesis: ( len p = 2 & p . 0 = x & p . 1 = y )
hence len p = (len <%x%>) + (len <%y%>) by Def4
.= 1 + (len <%y%>) by Th36
.= 1 + 1 by Th36
.= 2 ;
:: thesis: ( p . 0 = x & p . 1 = y )
A2: 0 in {0 } by TARSKI:def 1;
then 0 in dom <%x%> by Def5, CARD_1:87;
hence p . 0 = <%x%> . 0 by A1, Def4
.= x by Def5 ;
:: thesis: p . 1 = y
A3: 0 in dom <%y%> by A2, Def5, CARD_1:87;
thus p . 1 = (<%x%> ^ <%y%>) . ((len <%x%>) + 0 ) by A1, Th36
.= <%y%> . 0 by A3, Def4
.= y by Def5 ; :: thesis: verum

end;

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

proof

let k be Element of NAT ; :: thesis: ( k in dom <%x%> implies p . k = <%x%> . k )
assume k in dom <%x%> ; :: thesis: p . k = <%x%> . k
then k in {0 } by Def5, CARD_1:87;
then k = 0 by TARSKI:def 1;
hence p . k = <%x%> . k by A4, Def5; :: thesis: verum

end;

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

proof

let k be Element of 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 A7: k in {0 } by Def5, CARD_1:87;
thus p . ((len <%x%>) + k) = p . (1 + k) by Th36
.= p . (1 + 0 ) by A7, TARSKI:def 1
.= <%y%> . 0 by A4, Def5
.= <%y%> . k by A7, TARSKI:def 1 ; :: thesis: verum

end;

hence p = <%x,y%> by A5, A6, Def4; :: thesis: verum