set X = dom B;
set Y = dom C;
let T be Polish-language; :: thesis: ( T is C -compatible implies T is B -compatible )
assume A1: T is C -compatible ; :: thesis: T is B -compatible
let s be FinSequence; :: according to POLNOT_2:def 9 :: thesis: ( s in T & s is dom B -headed implies ex n being Nat st
( n = B . ((dom B) -head s) & (dom B) -tail s in T ^^ n ) )
assume that
A3: s in T and
A4: s is dom B -headed ; :: thesis: ex n being Nat st
( n = B . ((dom B) -head s) & (dom B) -tail s in T ^^ n )
A5: B c= C by Def3;
then A6: dom B c= dom C by GRFUNC_1:2;
then s is dom C -headed by A4;
then consider n being Nat such that
A10: ( n = C . ((dom C) -head s) & (dom C) -tail s in T ^^ n ) by A1, A3;
take n ; :: thesis: ( n = B . ((dom B) -head s) & (dom B) -tail s in T ^^ n )
( (dom B) -head s in dom B & (dom B) -head s = (dom C) -head s & (dom B) -tail s = (dom C) -tail s ) by A4, A6, POLNOT_1:55, POLNOT_1:def 22;
hence ( n = B . ((dom B) -head s) & (dom B) -tail s in T ^^ n ) by A5, A10, GRFUNC_1:2; :: thesis: verum