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, Th23
.= p by A1, Th17 ;
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;
S ^^ m = S by A7, Th8;
then A9: (S ^^ m) -tail r = q by A1, Th17;
(decomp (S,2,r)) . 2 = q by A8, A9, Th18;
hence decomp (S,2,r) = <*p,q*> by A5, Th54, FINSEQ_1:44; :: thesis: verum