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: 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
A4: ( m = u & M,v / (x. 0 ),m |= H ) by A2;
v / (x. 0 ),m in St H,M by A4, 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, Lm6;
hence u in { m where m is Element of M : {[{} ,m]} \/ ((v * decode ) | ((code (Free H)) \ {{} })) in Diagram H,M } by A4; :: thesis: verum

end;

{ 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
A5: ( m = u & {[{} ,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, Lm6;
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, A5; :: 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 A6: 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

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