let T be Polish-language; :: thesis: for U being T -extending Polish-language
for V being full Polish-language of T
for W being full Polish-language of U holds
( Polish-arity V c= Polish-arity W iff V c= W )
let U be T -extending Polish-language; :: thesis: for V being full Polish-language of T
for W being full Polish-language of U holds
( Polish-arity V c= Polish-arity W iff V c= W )
let V be full Polish-language of T; :: thesis: for W being full Polish-language of U holds
( Polish-arity V c= Polish-arity W iff V c= W )
let W be full Polish-language of U; :: thesis: ( Polish-arity V c= Polish-arity W iff V c= W )
A1: T c= U by Def9;
thus ( Polish-arity V c= Polish-arity W implies V c= W ) :: thesis: ( V c= W implies Polish-arity V c= Polish-arity W )
proof
assume A2: Polish-arity V c= Polish-arity W ; :: thesis: V c= W
set A = Polish-arity V;
set B = Polish-arity W;
A5: for a being object st a in T holds
(Polish-arity V) . a = (Polish-arity W) . a
proof
let a be object ; :: thesis: ( a in T implies (Polish-arity V) . a = (Polish-arity W) . a )
assume a in T ; :: thesis: (Polish-arity V) . a = (Polish-arity W) . a
then a in dom (Polish-arity V) by FUNCT_2:def 1;
hence (Polish-arity V) . a = (Polish-arity W) . a by A2, GRFUNC_1:2; :: thesis: verum
end;
defpred S1[ Nat] means Polish-expression-hierarchy (T,(Polish-arity V),$1) c= Polish-expression-hierarchy (U,(Polish-arity W),$1);
A10: S1[ 0 ]
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Polish-expression-hierarchy (T,(Polish-arity V),0) or a in Polish-expression-hierarchy (U,(Polish-arity W),0) )
assume a in Polish-expression-hierarchy (T,(Polish-arity V),0) ; :: thesis: a in Polish-expression-hierarchy (U,(Polish-arity W),0)
then a in Polish-atoms (T,(Polish-arity V)) by POLNOT_1:22;
then ( a in T & (Polish-arity V) . a = 0 ) by POLNOT_1:def 7;
then ( a in U & (Polish-arity W) . a = 0 ) by A1, A5;
then a in Polish-atoms (U,(Polish-arity W)) by POLNOT_1:def 7;
hence a in Polish-expression-hierarchy (U,(Polish-arity W),0) by POLNOT_1:22; :: thesis: verum
end;
A20: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
set G = Polish-expression-hierarchy (T,(Polish-arity V),k);
set H = Polish-expression-hierarchy (U,(Polish-arity W),k);
assume A21: S1[k] ; :: thesis: S1[k + 1]
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Polish-expression-hierarchy (T,(Polish-arity V),(k + 1)) or a in Polish-expression-hierarchy (U,(Polish-arity W),(k + 1)) )
assume a in Polish-expression-hierarchy (T,(Polish-arity V),(k + 1)) ; :: thesis: a in Polish-expression-hierarchy (U,(Polish-arity W),(k + 1))
then a in Polish-expression-layer (T,(Polish-arity V),(Polish-expression-hierarchy (T,(Polish-arity V),k))) by POLNOT_1:23;
then consider p, q being FinSequence, n being Nat such that
A23: a = p ^ q and
A24: p in T and
A25: n = (Polish-arity V) . p and
A26: q in (Polish-expression-hierarchy (T,(Polish-arity V),k)) ^^ n by POLNOT_1:def 6;
A27: ( p in U & n = (Polish-arity W) . p ) by A1, A5, A24, A25;
(Polish-expression-hierarchy (T,(Polish-arity V),k)) ^^ n c= (Polish-expression-hierarchy (U,(Polish-arity W),k)) ^^ n by A21, POLNOT_1:17;
then a in Polish-expression-layer (U,(Polish-arity W),(Polish-expression-hierarchy (U,(Polish-arity W),k))) by A23, A26, A27, POLNOT_1:18;
hence a in Polish-expression-hierarchy (U,(Polish-arity W),(k + 1)) by POLNOT_1:23; :: thesis: verum
end;
A30: for n being Nat holds S1[n] from NAT_1:sch 2(A10, A20);
 let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in V or a in W )
assume a in V ; :: thesis: a in W
then a in Polish-expression-set (T,(Polish-arity V)) ;
then consider n being Nat such that
A31: a in Polish-expression-hierarchy (T,(Polish-arity V),(n + 1)) by POLNOT_1:28;
Polish-expression-hierarchy (T,(Polish-arity V),(n + 1)) c= Polish-expression-hierarchy (U,(Polish-arity W),(n + 1)) by A30;
then a in Polish-expression-set (U,(Polish-arity W)) by A31, POLNOT_1:26, TARSKI:def 3;
hence a in W ; :: thesis: verum
end;
assume A40: V c= W ; :: thesis: Polish-arity V c= Polish-arity W
set A = Polish-arity V;
set B = Polish-arity W;
A41: ( dom (Polish-arity V) = T & dom (Polish-arity W) = U ) by FUNCT_2:def 1;
for a being object st a in dom (Polish-arity V) holds
(Polish-arity V) . a = (Polish-arity W) . a
proof
let a be object ; :: thesis: ( a in dom (Polish-arity V) implies (Polish-arity V) . a = (Polish-arity W) . a )
assume a in dom (Polish-arity V) ; :: thesis: (Polish-arity V) . a = (Polish-arity W) . a
then reconsider t = a as Element of T by FUNCT_2:def 1;
per cases ( U is trivial or not U is trivial ) ;
suppose not U is trivial ; :: thesis: (Polish-arity V) . a = (Polish-arity W) . a
then reconsider U = U as non trivial Polish-language ;
reconsider B = Polish-arity W as Polish-arity-function of U ;
set n = (Polish-arity V) . t;
set u = the Element of V ^^ ((Polish-arity V) . t);
set v = t ^ the Element of V ^^ ((Polish-arity V) . t);
A50: W = Polish-WFF-set (U,B) ;
V = Polish-WFF-set (T,(Polish-arity V)) ;
then V is -closed ;
then t ^ the Element of V ^^ ((Polish-arity V) . t) in Polish-expression-set (U,B) by A40;
then consider m being Nat, p, q being FinSequence such that
A52: p in U and
A53: m = B . p and
A54: q in W ^^ m and
A55: t ^ the Element of V ^^ ((Polish-arity V) . t) = p ^ q by POLNOT_1:32;
A56: V ^^ ((Polish-arity V) . t) c= W ^^ ((Polish-arity V) . t) by A40, POLNOT_1:17;
T c= U by Def9;
then t in U ;
then A57: ( p = t & the Element of V ^^ ((Polish-arity V) . t) = q ) by A52, A55, POLNOT_1:43;
then ( the Element of V ^^ ((Polish-arity V) . t) in W ^^ ((Polish-arity V) . t) & the Element of V ^^ ((Polish-arity V) . t) in W ^^ m ) by A54, A56;
hence (Polish-arity V) . a = (Polish-arity W) . a by A50, A53, A57, Lm3; :: thesis: verum
end;
end;
end;
hence Polish-arity V c= Polish-arity W by A41, Def9, GRFUNC_1:2; :: thesis: verum