let m, n be Nat; :: thesis: for S being Language holds S -formulasOfMaxDepth m c= S -formulasOfMaxDepth (m + n)
let S be Language; :: thesis: S -formulasOfMaxDepth m c= S -formulasOfMaxDepth (m + n)
set U = the non empty set ;
set X = S -formulasOfMaxDepth m;
set Y = S -formulasOfMaxDepth (m + n);
set II = the non empty set -InterpretersOf S;
set I = the Element of the non empty set -InterpretersOf S;
reconsider mm = m, NN = m + n as Element of NAT by ORDINAL1:def 12;
set f = ( the Element of the non empty set -InterpretersOf S,mm) -TruthEval ;
set g = ( the Element of the non empty set -InterpretersOf S,NN) -TruthEval ;
A1: ( S -formulasOfMaxDepth m = dom (( the Element of the non empty set -InterpretersOf S,mm) -TruthEval) & S -formulasOfMaxDepth (m + n) = dom (( the Element of the non empty set -InterpretersOf S,NN) -TruthEval) ) by Def22;
( the Element of the non empty set -InterpretersOf S,mm) -TruthEval c= ( the Element of the non empty set -InterpretersOf S,NN) -TruthEval by Lm12;
hence S -formulasOfMaxDepth m c= S -formulasOfMaxDepth (m + n) by GRFUNC_1:2, A1; :: thesis: verum