let S, T be Polish-language; :: thesis:
let n be Nat; :: thesis:
let s be Element of S ^^ n; :: thesis:
let t be Element of T ^^ n; :: thesis:
assume that
A1: S c= T and
A2: s = t ; :: thesis:
set p = decomp (S,n,s);
set q = decomp (T,n,t);
A4: ( dom (decomp (S,n,s)) = Seg n & dom (decomp (T,n,t)) = Seg n ) by Def32;
for a being object st a in Seg n holds
(decomp (S,n,s)) . a = (decomp (T,n,t)) . a

let a be object ; :: thesis:
assume A6: a in Seg n ; :: thesis:
then reconsider a = a as Nat ;
consider k being Nat such that
A7: a = k + 1 and
A8: (decomp (S,n,s)) . a = S -head ((S ^^ k) -tail s) by A6, Def32;
consider l being Nat such that
A9: a = l + 1 and
A10: (decomp (T,n,t)) . a = T -head ((T ^^ l) -tail t) by A6, Def32;
A11: S ^^ l c= T ^^ l by A1, Th17;
l + 1 <= n by A6, A9, FINSEQ_1:1;
then A12: ( s is S ^^ l -headed & (S ^^ l) -tail s is S -headed ) by Th57;
then A14: (T ^^ l) -tail t is S -headed by A2, A11, Th55;
(S ^^ k) -tail s = (T ^^ l) -tail t by A2, A7, A9, A11, A12, Th55;
hence (decomp (S,n,s)) . a = (decomp (T,n,t)) . a by A1, A8, A10, A14, Th55; :: thesis:

end;