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 :: thesis: Section (H,v) = { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) }

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 object ; :: 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:36;
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 object ; :: 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; :: 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 :: thesis: not { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) } <> {}

set u = the 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 the Element of { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) } 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 = the Element of { m where m is Element of M : {[{},m]} \/ ((v * decode) | ((code (Free H)) \ {{}})) in Diagram (H,M) } 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:1;
then {} in (dom (v2 * decode)) /\ (code (Free H)) by A10, RELAT_1:61;
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:33;
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