let H be ZF-formula; :: thesis: for M being non empty set
for v being Function of VAR ,M holds Section H,v = { m where m is Element of M : {[{} ,m]} \/ ((v * decode ) | ((code (Free H)) \ {{} })) in Diagram H,M }
let M be non empty set ; :: thesis: for v being Function of VAR ,M holds Section H,v = { m where m is Element of M : {[{} ,m]} \/ ((v * decode ) | ((code (Free H)) \ {{} })) in Diagram H,M }
let v be Function of VAR ,M; :: thesis: Section H,v = { m where m is Element of M : {[{} ,m]} \/ ((v * decode ) | ((code (Free H)) \ {{} })) in Diagram H,M }
set S = Section H,v;
set D = { m where m is Element of M : {[{} ,m]} \/ ((v * decode ) | ((code (Free H)) \ {{} })) in Diagram H,M } ;

now

per cases ( x. 0 in Free H or not x. 0 in Free H ) ;

suppose A1: x. 0 in Free H ; :: thesis: Section H,v = { m where m is Element of M : {[{} ,m]} \/ ((v * decode ) | ((code (Free H)) \ {{} })) in Diagram H,M }

then A2: Section H,v = { m where m is Element of M : M,v / (x. 0 ),m |= H } by Def1;
A3: { m where m is Element of M : {[{} ,m]} \/ ((v * decode ) | ((code (Free H)) \ {{} })) in Diagram H,M } c= Section H,v

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in { m where m is Element of M : {[{} ,m]} \/ ((v * decode ) | ((code (Free H)) \ {{} })) in Diagram H,M } or u in Section H,v )
assume u in { m where m is Element of M : {[{} ,m]} \/ ((v * decode ) | ((code (Free H)) \ {{} })) in Diagram H,M } ; :: thesis: u in Section H,v
then consider m being Element of M such that
A4: m = u and
A5: {[{} ,m]} \/ ((v * decode ) | ((code (Free H)) \ {{} })) in Diagram H,M ;
((v / (x. 0 ),m) * decode ) | (code (Free H)) in Diagram H,M by A1, A5, Lm5;
then ex v1 being Function of VAR ,M st
( ((v / (x. 0 ),m) * decode ) | (code (Free H)) = (v1 * decode ) | (code (Free H)) & v1 in St H,M ) by ZF_FUND1:def 5;
then v / (x. 0 ),m in St H,M by ZF_FUND1:37;
then M,v / (x. 0 ),m |= H by ZF_MODEL:def 4;
hence u in Section H,v by A2, A4; :: thesis: verum

end;

Section H,v c= { m where m is Element of M : {[{} ,m]} \/ ((v * decode ) | ((code (Free H)) \ {{} })) in Diagram H,M }

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in Section H,v or u in { m where m is Element of M : {[{} ,m]} \/ ((v * decode ) | ((code (Free H)) \ {{} })) in Diagram H,M } )
assume u in Section H,v ; :: thesis: u in { m where m is Element of M : {[{} ,m]} \/ ((v * decode ) | ((code (Free H)) \ {{} })) in Diagram H,M }
then consider m being Element of M such that
A6: m = u and
A7: M,v / (x. 0 ),m |= H by A2;
v / (x. 0 ),m in St H,M by A7, ZF_MODEL:def 4;
then ((v / (x. 0 ),m) * decode ) | (code (Free H)) in Diagram H,M by ZF_FUND1:def 5;
then {[{} ,m]} \/ ((v * decode ) | ((code (Free H)) \ {{} })) in Diagram H,M by A1, Lm5;
hence u in { m where m is Element of M : {[{} ,m]} \/ ((v * decode ) | ((code (Free H)) \ {{} })) in Diagram H,M } by A6; :: thesis: verum

end;

hence Section H,v = { m where m is Element of M : {[{} ,m]} \/ ((v * decode ) | ((code (Free H)) \ {{} })) in Diagram H,M } by A3, XBOOLE_0:def 10; :: thesis: verum

end;

suppose A8: not x. 0 in Free H ; :: thesis: Section H,v = { m where m is Element of M : {[{} ,m]} \/ ((v * decode ) | ((code (Free H)) \ {{} })) in Diagram H,M }

now

consider u being Element of { m where m is Element of M : {[{} ,m]} \/ ((v * decode ) | ((code (Free H)) \ {{} })) in Diagram H,M } ;
assume { m where m is Element of M : {[{} ,m]} \/ ((v * decode ) | ((code (Free H)) \ {{} })) in Diagram H,M } <> {} ; :: thesis: contradiction
then u in { m where m is Element of M : {[{} ,m]} \/ ((v * decode ) | ((code (Free H)) \ {{} })) in Diagram H,M } ;
then consider m being Element of M such that
m = u and
A9: {[{} ,m]} \/ ((v * decode ) | ((code (Free H)) \ {{} })) in Diagram H,M ;
consider v2 being Function of VAR ,M such that
A10: {[{} ,m]} \/ ((v * decode ) | ((code (Free H)) \ {{} })) = (v2 * decode ) | (code (Free H)) and
v2 in St H,M by A9, ZF_FUND1:def 5;
reconsider w = {[{} ,m]} \/ ((v * decode ) | ((code (Free H)) \ {{} })) as Function by A10;
[{} ,m] in {[{} ,m]} by TARSKI:def 1;
then [{} ,m] in w by XBOOLE_0:def 3;
then {} in dom w by FUNCT_1:8;
then {} in (dom (v2 * decode )) /\ (code (Free H)) by A10, RELAT_1:90;
then {} in code (Free H) by XBOOLE_0:def 4;
then ex y being Variable st
( y in Free H & {} = x". y ) by ZF_FUND1:34;
hence contradiction by A8, ZF_FUND1:def 3; :: thesis: verum

end;

hence Section H,v = { m where m is Element of M : {[{} ,m]} \/ ((v * decode ) | ((code (Free H)) \ {{} })) in Diagram H,M } by A8, Def1; :: thesis: verum

end;

end;

end;

hence Section H,v = { m where m is Element of M : {[{} ,m]} \/ ((v * decode ) | ((code (Free H)) \ {{} })) in Diagram H,M } ; :: thesis: verum