let V be Universe; :: thesis:
let X be Subclass of V; :: thesis:
let E be non empty set ; :: thesis:
assume that
A1: X is closed_wrt_A1-A7 and
A2: E in X ; :: thesis:
let H be ZF-formula; :: thesis:
let v1 be Element of VAR ; :: thesis:
assume A3: Diagram H,E in X ; :: thesis:

per cases ;

suppose A4: not v1 in Free H ; :: thesis:

then Free H = (Free H) \ {v1} by ZFMISC_1:65;
then A5: Free (All v1,H) = Free H by ZF_LANG1:67;
Diagram (All v1,H),E = Diagram H,E

proof

thus Diagram (All v1,H),E c= Diagram H,E :: according to XBOOLE_0:def 10 :: thesis:

proof

let p be set ; :: according to TARSKI:def 3 :: thesis:
assume p in Diagram (All v1,H),E ; :: thesis:
then consider f being Function of VAR ,E such that
A6: p = (f * decode ) | (code (Free (All v1,H))) and
A7: f in St (All v1,H),E by Def5;
f in St H,E by A7, ZF_MODEL:6;
hence p in Diagram H,E by A5, A6, Def5; :: thesis:

end;

let p be set ; :: according to TARSKI:def 3 :: thesis:
assume p in Diagram H,E ; :: thesis:
then consider f being Function of VAR ,E such that
A8: p = (f * decode ) | (code (Free H)) and
A9: f in St H,E by Def5;
for g being Function of VAR ,E st ( for v2 being Element of VAR st g . v2 <> f . v2 holds
v1 = v2 ) holds
g in St H,E

proof

let g be Function of VAR ,E; :: thesis:
assume for v2 being Element of VAR st g . v2 <> f . v2 holds
v1 = v2 ; :: thesis:
then A10: for v2 being Element of VAR st v2 in Free H holds
f . v2 = g . v2 by A4;
E,f |= H by A9, ZF_MODEL:def 4;
then E,g |= H by A10, ZF_LANG1:84;
hence g in St H,E by ZF_MODEL:def 4; :: thesis:

end;

then f in St (All v1,H),E by A9, ZF_MODEL:6;
hence p in Diagram (All v1,H),E by A5, A8, Def5; :: thesis:

end;

hence Diagram (All v1,H),E in X by A3; :: thesis:

end;

suppose A11: v1 in Free H ; :: thesis:

reconsider m = E as Element of V by A2;
set n = x". v1;
set fs = code (Free H);
A12: Diagram ('not' H),E c= Funcs (code (Free H)),E

proof

let p be set ; :: according to TARSKI:def 3 :: thesis:
assume p in Diagram ('not' H),E ; :: thesis:
then A13: ex f being Function of VAR ,E st
( p = (f * decode ) | (code (Free ('not' H))) & f in St ('not' H),E ) by Def5;
Free ('not' H) = Free H by ZF_LANG1:65;
hence p in Funcs (code (Free H)),E by A13, Lm3; :: thesis:

end;

A14: (code (Free H)) \ {(x". v1)} = (code (Free H)) \ (code {v1}) by Lm6
.= code ((Free H) \ {v1}) by Lm1, FUNCT_1:123 ;
then A15: (code (Free H)) \ {(x". v1)} = code (Free (All v1,H)) by ZF_LANG1:67;
A16: Diagram ('not' H),E in X by A1, A2, A3, Th19;
then reconsider Dn = Diagram ('not' H),E as Element of V ;
set C = { x where x is Element of V : ( x in Funcs ((code (Free H)) \ {(x". v1)}),m & ex u being set st {[(x". v1),u]} \/ x in Dn ) } ;
A17: Funcs ((code (Free H)) \ {(x". v1)}),m in X by A1, A2, Th9;
{v1} c= Free H by A11, ZFMISC_1:37;
then Free H = ((Free H) \ {v1}) \/ {v1} by XBOOLE_1:45;
then A18: code (Free H) = (code ((Free H) \ {v1})) \/ (code {v1}) by RELAT_1:153
.= (code ((Free H) \ {v1})) \/ {(x". v1)} by Lm6 ;
A19: (Funcs ((code (Free H)) \ {(x". v1)}),m) \ { x where x is Element of V : ( x in Funcs ((code (Free H)) \ {(x". v1)}),m & ex u being set st {[(x". v1),u]} \/ x in Dn ) } = Diagram (All v1,H),E

proof

thus (Funcs ((code (Free H)) \ {(x". v1)}),m) \ { x where x is Element of V : ( x in Funcs ((code (Free H)) \ {(x". v1)}),m & ex u being set st {[(x". v1),u]} \/ x in Dn ) } c= Diagram (All v1,H),E :: according to XBOOLE_0:def 10 :: thesis:

proof

let p be set ; :: according to TARSKI:def 3 :: thesis:
assume A20: p in (Funcs ((code (Free H)) \ {(x". v1)}),m) \ { x where x is Element of V : ( x in Funcs ((code (Free H)) \ {(x". v1)}),m & ex u being set st {[(x". v1),u]} \/ x in Dn ) } ; :: thesis:
then consider h being Function such that
A21: p = h and
dom h = (code (Free H)) \ {(x". v1)} and
rng h c= E by FUNCT_2:def 2;
consider f being Function of VAR ,E such that
A22: h = (f * decode ) | ((code (Free H)) \ {(x". v1)}) by A20, A21, Lm11;
A23: not p in { x where x is Element of V : ( x in Funcs ((code (Free H)) \ {(x". v1)}),m & ex u being set st {[(x". v1),u]} \/ x in Dn ) } by A20, XBOOLE_0:def 5;
f in St (All v1,H),E

proof

assume A24: not f in St (All v1,H),E ; :: thesis:
A25: for ff being Function of VAR ,E st p = (ff * decode ) | (code (Free (All v1,H))) holds
ff in St H,E

proof

let ff be Function of VAR ,E; :: thesis:
assume A26: p = (ff * decode ) | (code (Free (All v1,H))) ; :: thesis:
(ff * decode ) | ((code (Free H)) \ {(x". v1)}) in Funcs ((code (Free H)) \ {(x". v1)}),m by Lm3;
then reconsider x = (ff * decode ) | ((code (Free H)) \ {(x". v1)}) as Element of V by A17, Th1;
assume not ff in St H,E ; :: thesis:
then ff in St ('not' H),E by ZF_MODEL:4;
then (ff * decode ) | (code (Free ('not' H))) in Dn by Def5;
then (ff * decode ) | (((code (Free H)) \ {(x". v1)}) \/ {(x". v1)}) in Dn by A18, A14, ZF_LANG1:65;
then A27: ((ff * decode ) | ((code (Free H)) \ {(x". v1)})) \/ ((ff * decode ) | {(x". v1)}) in Dn by RELAT_1:107;
dom ((ff * decode ) | {(x". v1)}) = {(x". v1)} by Lm3;
then {[(x". v1),(((ff * decode ) | {(x". v1)}) . (x". v1))]} \/ x in Dn by A27, GRFUNC_1:18;
hence contradiction by A15, A20, A23, A26; :: thesis:

end;

then f in St H,E by A15, A21, A22;
then consider e being Function of VAR ,E such that
A28: for v2 being Element of VAR st e . v2 <> f . v2 holds
v2 = v1 and
A29: not e in St H,E by A24, ZF_MODEL:6;

now

thus A30: ( (code (Free H)) \ {(x". v1)} = dom ((e * decode ) | ((code (Free H)) \ {(x". v1)})) & (code (Free H)) \ {(x". v1)} = dom ((f * decode ) | ((code (Free H)) \ {(x". v1)})) ) by Lm3; :: thesis:
let q be set ; :: thesis:
assume A31: q in (code (Free H)) \ {(x". v1)} ; :: thesis:
then reconsider p99 = q as Element of omega ;
A32: q = x". (x. (card p99)) by Lm2;
not q in {(x". v1)} by A31, XBOOLE_0:def 5;
then A33: x. (card p99) <> v1 by A32, TARSKI:def 1;
thus ((e * decode ) | ((code (Free H)) \ {(x". v1)})) . q = (e * decode ) . q by A30, A31, FUNCT_1:70
.= e . (x. (card p99)) by A32, Lm4
.= f . (x. (card p99)) by A28, A33
.= (f * decode ) . q by A32, Lm4
.= ((f * decode ) | ((code (Free H)) \ {(x". v1)})) . q by A30, A31, FUNCT_1:70 ; :: thesis:

end;

hence contradiction by A15, A21, A22, A25, A29, FUNCT_1:9; :: thesis:

end;

hence p in Diagram (All v1,H),E by A15, A21, A22, Def5; :: thesis:

end;

let p be set ; :: according to TARSKI:def 3 :: thesis:
assume p in Diagram (All v1,H),E ; :: thesis:
then consider f being Function of VAR ,E such that
A34: p = (f * decode ) | (code (Free (All v1,H))) and
A35: f in St (All v1,H),E by Def5;
A36: p in Funcs ((code (Free H)) \ {(x". v1)}),m by A15, A34, Lm3;
then reconsider x = p as Element of V by A17, Th1;

A37: now

A38: code (Free H) = code (Free ('not' H)) by ZF_LANG1:65;
given u being set such that A39: {[(x". v1),u]} \/ x in Dn ; :: thesis:
consider h being Function of VAR ,E such that
A40: {[(x". v1),u]} \/ x = (h * decode ) | (code (Free H)) by A12, A39, Lm11;

now

end;

then A44: h in St (All v1,H),E by A15, A35, Lm10, FUNCT_1:9;
ex hh being Function of VAR ,E st
( {[(x". v1),u]} \/ x = (hh * decode ) | (code (Free ('not' H))) & hh in St ('not' H),E ) by A39, Def5;
then h in St ('not' H),E by A40, A38, Lm10;
then not h in St H,E by ZF_MODEL:4;
hence contradiction by A44, ZF_MODEL:6; :: thesis:

end;

now

assume x in { x where x is Element of V : ( x in Funcs ((code (Free H)) \ {(x". v1)}),m & ex u being set st {[(x". v1),u]} \/ x in Dn ) } ; :: thesis:
then ex y being Element of V st
( y = x & y in Funcs ((code (Free H)) \ {(x". v1)}),m & ex u being set st {[(x". v1),u]} \/ y in Dn ) ;
hence contradiction by A37; :: thesis:

end;

hence p in (Funcs ((code (Free H)) \ {(x". v1)}),m) \ { x where x is Element of V : ( x in Funcs ((code (Free H)) \ {(x". v1)}),m & ex u being set st {[(x". v1),u]} \/ x in Dn ) } by A36, XBOOLE_0:def 5; :: thesis:

end;

x". v1 in code (Free H) by A11, Lm5;
then { x where x is Element of V : ( x in Funcs ((code (Free H)) \ {(x". v1)}),m & ex u being set st {[(x". v1),u]} \/ x in Dn ) } in X by A1, A2, A16, A12, Th11;
hence Diagram (All v1,H),E in X by A1, A17, A19, Th4; :: thesis:

end;