let m be Nat; :: thesis: for S being Language
for w2 being string of S
for U being non empty set
for phi1 being wff string of S
for I being Element of U -InterpretersOf S
for f being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN st dom f = [:(U -InterpretersOf S),(S -formulasOfMaxDepth m):] & phi1 is m -wff holds
( f -NorFunctor (I,((<*(TheNorSymbOf S)*> ^ phi1) ^ w2)) = 1 iff ( f . (I,phi1) = 0 & f . (I,w2) = 0 ) )
let S be Language; :: thesis: for w2 being string of S
for U being non empty set
for phi1 being wff string of S
for I being Element of U -InterpretersOf S
for f being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN st dom f = [:(U -InterpretersOf S),(S -formulasOfMaxDepth m):] & phi1 is m -wff holds
( f -NorFunctor (I,((<*(TheNorSymbOf S)*> ^ phi1) ^ w2)) = 1 iff ( f . (I,phi1) = 0 & f . (I,w2) = 0 ) )
let w2 be string of S; :: thesis: for U being non empty set
for phi1 being wff string of S
for I being Element of U -InterpretersOf S
for f being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN st dom f = [:(U -InterpretersOf S),(S -formulasOfMaxDepth m):] & phi1 is m -wff holds
( f -NorFunctor (I,((<*(TheNorSymbOf S)*> ^ phi1) ^ w2)) = 1 iff ( f . (I,phi1) = 0 & f . (I,w2) = 0 ) )
let U be non empty set ; :: thesis: for phi1 being wff string of S
for I being Element of U -InterpretersOf S
for f being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN st dom f = [:(U -InterpretersOf S),(S -formulasOfMaxDepth m):] & phi1 is m -wff holds
( f -NorFunctor (I,((<*(TheNorSymbOf S)*> ^ phi1) ^ w2)) = 1 iff ( f . (I,phi1) = 0 & f . (I,w2) = 0 ) )
let phi1 be wff string of S; :: thesis: for I being Element of U -InterpretersOf S
for f being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN st dom f = [:(U -InterpretersOf S),(S -formulasOfMaxDepth m):] & phi1 is m -wff holds
( f -NorFunctor (I,((<*(TheNorSymbOf S)*> ^ phi1) ^ w2)) = 1 iff ( f . (I,phi1) = 0 & f . (I,w2) = 0 ) )
let I be Element of U -InterpretersOf S; :: thesis: for f being PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN st dom f = [:(U -InterpretersOf S),(S -formulasOfMaxDepth m):] & phi1 is m -wff holds
( f -NorFunctor (I,((<*(TheNorSymbOf S)*> ^ phi1) ^ w2)) = 1 iff ( f . (I,phi1) = 0 & f . (I,w2) = 0 ) )
set II = U -InterpretersOf S;
set SS = AllSymbolsOf S;
set N = TheNorSymbOf S;
set phi2 = w2;
set psi = (<*(TheNorSymbOf S)*> ^ phi1) ^ w2;
set FF = AllFormulasOf S;
set Phim = S -formulasOfMaxDepth m;
let f be PartFunc of [:(U -InterpretersOf S),(((AllSymbolsOf S) *) \ {{}}):],BOOLEAN; :: thesis: ( dom f = [:(U -InterpretersOf S),(S -formulasOfMaxDepth m):] & phi1 is m -wff implies ( f -NorFunctor (I,((<*(TheNorSymbOf S)*> ^ phi1) ^ w2)) = 1 iff ( f . (I,phi1) = 0 & f . (I,w2) = 0 ) ) )
assume A1: ( dom f = [:(U -InterpretersOf S),(S -formulasOfMaxDepth m):] & phi1 is m -wff ) ; :: thesis: ( f -NorFunctor (I,((<*(TheNorSymbOf S)*> ^ phi1) ^ w2)) = 1 iff ( f . (I,phi1) = 0 & f . (I,w2) = 0 ) )
set LH = f -NorFunctor (I,((<*(TheNorSymbOf S)*> ^ phi1) ^ w2));
set RH1 = f . (I,phi1);
set RH2 = f . (I,w2);

hereby :: thesis: ( f . (I,phi1) = 0 & f . (I,w2) = 0 implies f -NorFunctor (I,((<*(TheNorSymbOf S)*> ^ phi1) ^ w2)) = 1 )

assume f -NorFunctor (I,((<*(TheNorSymbOf S)*> ^ phi1) ^ w2)) = 1 ; :: thesis: ( f . (I,phi1) = 0 & f . (I,w2) = 0 )
then consider w, w1 being string of S such that
A2: ( [I,w] in dom f & f . (I,w) = FALSE & f . (I,w1) = FALSE & (<*(TheNorSymbOf S)*> ^ phi1) ^ w2 = (<*(TheNorSymbOf S)*> ^ w) ^ w1 ) by Def17;
A3: ( w in S -formulasOfMaxDepth m & phi1 in S -formulasOfMaxDepth m ) by A1, A2, ZFMISC_1:87;
<*(TheNorSymbOf S)*> ^ (w ^ w1) = (<*(TheNorSymbOf S)*> ^ phi1) ^ w2 by A2, FINSEQ_1:32
.= <*(TheNorSymbOf S)*> ^ (phi1 ^ w2) by FINSEQ_1:32 ;
then w ^ w1 = phi1 ^ w2 by FINSEQ_1:33;
hence ( f . (I,phi1) = 0 & f . (I,w2) = 0 ) by A2, FOMODEL0:def 19, A3; :: thesis: verum

end;

assume ( f . (I,phi1) = 0 & f . (I,w2) = 0 ) ; :: thesis: f -NorFunctor (I,((<*(TheNorSymbOf S)*> ^ phi1) ^ w2)) = 1
hence f -NorFunctor (I,((<*(TheNorSymbOf S)*> ^ phi1) ^ w2)) = 1 by A1, ZFMISC_1:87, Def17; :: thesis: verum