let S be Polish-language; :: thesis: for p, q being Element of S
for r being Element of S ^^ 2 st r = p ^ q holds
decomp (S,2,r) = <*p,q*>
let p, q be Element of S; :: thesis: for r being Element of S ^^ 2 st r = p ^ q holds
decomp (S,2,r) = <*p,q*>
let r be Element of S ^^ 2; :: thesis: ( r = p ^ q implies decomp (S,2,r) = <*p,q*> )
assume A1: r = p ^ q ; :: thesis: decomp (S,2,r) = <*p,q*>
set w = decomp (S,2,r);
1 in Seg 2 by FINSEQ_1:2, TARSKI:def 2;
then consider k being Nat such that
A2: 1 = k + 1 and
A3: (decomp (S,2,r)) . 1 = S -head ((S ^^ k) -tail r) by Def32;
A5: (decomp (S,2,r)) . 1 = S -head r by A2, A3, Th58
.= p by A1 ;
2 in Seg 2 by FINSEQ_1:2, TARSKI:def 2;
then consider m being Nat such that
A7: 2 = m + 1 and
A8: (decomp (S,2,r)) . 2 = S -head ((S ^^ m) -tail r) by Def32;
thus decomp (S,2,r) = <*p,q*> by A1, A5, A7, A8, Th62, FINSEQ_1:44; :: thesis: verum