:: ZF_FUND1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

definition
let A, B be set ;
func A (#) B -> set means :Def1: :: ZF_FUND1:def 1
for p being set holds
( p in it iff ex q, r, s being set st
( p = [q,s] & [q,r] in A & [r,s] in B ) );
existence
ex b1 being set st
for p being set holds
( p in b1 iff ex q, r, s being set st
( p = [q,s] & [q,r] in A & [r,s] in B ) )
proof end;
uniqueness
for b1, b2 being set st ( for p being set holds
( p in b1 iff ex q, r, s being set st
( p = [q,s] & [q,r] in A & [r,s] in B ) ) ) & ( for p being set holds
( p in b2 iff ex q, r, s being set st
( p = [q,s] & [q,r] in A & [r,s] in B ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines (#) ZF_FUND1:def 1 :
for A, B, b3 being set holds
( b3 = A (#) B iff for p being set holds
( p in b3 iff ex q, r, s being set st
( p = [q,s] & [q,r] in A & [r,s] in B ) ) );

definition
let V be Universe;
let x, y be Element of V;
:: original: (#)
redefine func x (#) y -> Element of V;
coherence
x (#) y is Element of V
proof end;
end;

definition
func decode -> Function of omega , VAR means :Def2: :: ZF_FUND1:def 2
for p being Element of omega holds it . p = x. (card p);
existence
ex b1 being Function of omega , VAR st
for p being Element of omega holds b1 . p = x. (card p)
proof end;
uniqueness
for b1, b2 being Function of omega , VAR st ( for p being Element of omega holds b1 . p = x. (card p) ) & ( for p being Element of omega holds b2 . p = x. (card p) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines decode ZF_FUND1:def 2 :
for b1 being Function of omega , VAR holds
( b1 = decode iff for p being Element of omega holds b1 . p = x. (card p) );

definition
let v1 be Element of VAR ;
func x". v1 -> Nat means :Def3: :: ZF_FUND1:def 3
x. it = v1;
existence
ex b1 being Nat st x. b1 = v1
proof end;
uniqueness
for b1, b2 being Nat st x. b1 = v1 & x. b2 = v1 holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines x". ZF_FUND1:def 3 :
for v1 being Element of VAR
for b2 being Nat holds
( b2 = x". v1 iff x. b2 = v1 );

Lm1: ( dom decode = omega & rng decode = VAR & decode is one-to-one & decode " is one-to-one & dom (decode " ) = VAR & rng (decode " ) = omega )
proof end;

definition
let A be finite Subset of VAR ;
func code A -> finite Subset of omega equals :: ZF_FUND1:def 4
(decode " ) .: A;
coherence
(decode " ) .: A is finite Subset of omega
by Lm1, RELAT_1:144;
end;

:: deftheorem defines code ZF_FUND1:def 4 :
for A being finite Subset of VAR holds code A = (decode " ) .: A;

definition
let H be ZF-formula;
:: original: Free
redefine func Free H -> finite Subset of VAR ;
coherence
Free H is finite Subset of VAR
by ZF_LANG1:85;
end;

definition
let n be Element of omega ;
:: original: {
redefine func {n} -> finite Subset of omega ;
coherence
{n} is finite Subset of omega
by ZFMISC_1:37;
end;

definition
let v1 be Element of VAR ;
:: original: {
redefine func {v1} -> finite Subset of VAR ;
coherence
{v1} is finite Subset of VAR
by ZFMISC_1:37;
let v2 be Element of VAR ;
:: original: {
redefine func {v1,v2} -> finite Subset of VAR ;
coherence
{v1,v2} is finite Subset of VAR
by ZFMISC_1:38;
end;

definition
let H be ZF-formula;
let E be non empty set ;
func Diagram H,E -> set means :Def5: :: ZF_FUND1:def 5
for p being set holds
( p in it iff ex f being Function of VAR ,E st
( p = (f * decode ) | (code (Free H)) & f in St H,E ) );
existence
ex b1 being set st
for p being set holds
( p in b1 iff ex f being Function of VAR ,E st
( p = (f * decode ) | (code (Free H)) & f in St H,E ) )
proof end;
uniqueness
for b1, b2 being set st ( for p being set holds
( p in b1 iff ex f being Function of VAR ,E st
( p = (f * decode ) | (code (Free H)) & f in St H,E ) ) ) & ( for p being set holds
( p in b2 iff ex f being Function of VAR ,E st
( p = (f * decode ) | (code (Free H)) & f in St H,E ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def5 defines Diagram ZF_FUND1:def 5 :
for H being ZF-formula
for E being non empty set
for b3 being set holds
( b3 = Diagram H,E iff for p being set holds
( p in b3 iff ex f being Function of VAR ,E st
( p = (f * decode ) | (code (Free H)) & f in St H,E ) ) );

definition
let V be Universe;
let X be Subclass of V;
attr X is closed_wrt_A1 means :Def6: :: ZF_FUND1:def 6
for a being Element of V st a in X holds
{ {[(0-element_of V),x],[(1-element_of V),y]} where x, y is Element of V : ( x in y & x in a & y in a ) } in X;
attr X is closed_wrt_A2 means :Def7: :: ZF_FUND1:def 7
for a, b being Element of V st a in X & b in X holds
{a,b} in X;
attr X is closed_wrt_A3 means :Def8: :: ZF_FUND1:def 8
for a being Element of V st a in X holds
union a in X;
attr X is closed_wrt_A4 means :Def9: :: ZF_FUND1:def 9
for a, b being Element of V st a in X & b in X holds
{ {[x,y]} where x, y is Element of V : ( x in a & y in b ) } in X;
attr X is closed_wrt_A5 means :Def10: :: ZF_FUND1:def 10
for a, b being Element of V st a in X & b in X holds
{ (x \/ y) where x, y is Element of V : ( x in a & y in b ) } in X;
attr X is closed_wrt_A6 means :Def11: :: ZF_FUND1:def 11
for a, b being Element of V st a in X & b in X holds
{ (x \ y) where x, y is Element of V : ( x in a & y in b ) } in X;
attr X is closed_wrt_A7 means :Def12: :: ZF_FUND1:def 12
for a, b being Element of V st a in X & b in X holds
{ (x (#) y) where x, y is Element of V : ( x in a & y in b ) } in X;
end;

:: deftheorem Def6 defines closed_wrt_A1 ZF_FUND1:def 6 :
for V being Universe
for X being Subclass of V holds
( X is closed_wrt_A1 iff for a being Element of V st a in X holds
{ {[(0-element_of V),x],[(1-element_of V),y]} where x, y is Element of V : ( x in y & x in a & y in a ) } in X );

:: deftheorem Def7 defines closed_wrt_A2 ZF_FUND1:def 7 :
for V being Universe
for X being Subclass of V holds
( X is closed_wrt_A2 iff for a, b being Element of V st a in X & b in X holds
{a,b} in X );

:: deftheorem Def8 defines closed_wrt_A3 ZF_FUND1:def 8 :
for V being Universe
for X being Subclass of V holds
( X is closed_wrt_A3 iff for a being Element of V st a in X holds
union a in X );

:: deftheorem Def9 defines closed_wrt_A4 ZF_FUND1:def 9 :
for V being Universe
for X being Subclass of V holds
( X is closed_wrt_A4 iff for a, b being Element of V st a in X & b in X holds
{ {[x,y]} where x, y is Element of V : ( x in a & y in b ) } in X );

:: deftheorem Def10 defines closed_wrt_A5 ZF_FUND1:def 10 :
for V being Universe
for X being Subclass of V holds
( X is closed_wrt_A5 iff for a, b being Element of V st a in X & b in X holds
{ (x \/ y) where x, y is Element of V : ( x in a & y in b ) } in X );

:: deftheorem Def11 defines closed_wrt_A6 ZF_FUND1:def 11 :
for V being Universe
for X being Subclass of V holds
( X is closed_wrt_A6 iff for a, b being Element of V st a in X & b in X holds
{ (x \ y) where x, y is Element of V : ( x in a & y in b ) } in X );

:: deftheorem Def12 defines closed_wrt_A7 ZF_FUND1:def 12 :
for V being Universe
for X being Subclass of V holds
( X is closed_wrt_A7 iff for a, b being Element of V st a in X & b in X holds
{ (x (#) y) where x, y is Element of V : ( x in a & y in b ) } in X );

definition
let V be Universe;
let X be Subclass of V;
attr X is closed_wrt_A1-A7 means :Def13: :: ZF_FUND1:def 13
( X is closed_wrt_A1 & X is closed_wrt_A2 & X is closed_wrt_A3 & X is closed_wrt_A4 & X is closed_wrt_A5 & X is closed_wrt_A6 & X is closed_wrt_A7 );
end;

:: deftheorem Def13 defines closed_wrt_A1-A7 ZF_FUND1:def 13 :
for V being Universe
for X being Subclass of V holds
( X is closed_wrt_A1-A7 iff ( X is closed_wrt_A1 & X is closed_wrt_A2 & X is closed_wrt_A3 & X is closed_wrt_A4 & X is closed_wrt_A5 & X is closed_wrt_A6 & X is closed_wrt_A7 ) );

Lm2: for A being Element of omega holds A = x". (x. (card A))
proof end;

Lm3: for fs being finite Subset of omega
for E being non empty set
for f being Function of VAR ,E holds
( dom ((f * decode ) | fs) = fs & rng ((f * decode ) | fs) c= E & (f * decode ) | fs in Funcs fs,E & dom (f * decode ) = omega & rng (f * decode ) c= E )
proof end;

Lm4: for E being non empty set
for f being Function of VAR ,E
for v1 being Element of VAR holds
( decode . (x". v1) = v1 & (decode " ) . v1 = x". v1 & (f * decode ) . (x". v1) = f . v1 )
proof end;

Lm5: for p being set
for A being finite Subset of VAR holds
( p in code A iff ex v1 being Element of VAR st
( v1 in A & p = x". v1 ) )
proof end;

Lm6: for v1 being Element of VAR holds code {v1} = {(x". v1)}
proof end;

Lm7: for v1, v2 being Element of VAR holds code {v1,v2} = {(x". v1),(x". v2)}
proof end;

Lm8: for A being finite Subset of VAR holds A, code A are_equipotent
proof end;

Lm9: for A, B being finite Subset of VAR holds
( code (A \/ B) = (code A) \/ (code B) & code (A \ B) = (code A) \ (code B) )
by RELAT_1:153, Lm1, FUNCT_1:123;

Lm10: for E being non empty set
for f being Function of VAR ,E
for v1 being Element of VAR
for H being ZF-formula st v1 in Free H holds
((f * decode ) | (code (Free H))) . (x". v1) = f . v1
proof end;

Lm11: for E being non empty set
for H being ZF-formula
for f, g being Function of VAR ,E st (f * decode ) | (code (Free H)) = (g * decode ) | (code (Free H)) & f in St H,E holds
g in St H,E
proof end;

Lm12: for p being set
for fs being finite Subset of omega
for E being non empty set st p in Funcs fs,E holds
ex f being Function of VAR ,E st p = (f * decode ) | fs
proof end;

theorem Th1: :: ZF_FUND1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being Universe
for X being Subclass of V
for o, A being set holds
( X c= V & ( o in X implies o is Element of V ) & ( o in A & A in X implies o is Element of V ) )
proof end;

theorem Th2: :: ZF_FUND1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being Universe
for X being Subclass of V
for o, A being set st X is closed_wrt_A1-A7 holds
( ( o in X implies {o} in X ) & ( {o} in X implies o in X ) & ( A in X implies union A in X ) )
proof end;

theorem Th3: :: ZF_FUND1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being Universe
for X being Subclass of V st X is closed_wrt_A1-A7 holds
{} in X
proof end;

theorem Th4: :: ZF_FUND1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being Universe
for X being Subclass of V
for A, B being set st X is closed_wrt_A1-A7 & A in X & B in X holds
( A \/ B in X & A \ B in X & A (#) B in X )
proof end;

theorem Th5: :: ZF_FUND1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being Universe
for X being Subclass of V
for A, B being set st X is closed_wrt_A1-A7 & A in X & B in X holds
A /\ B in X
proof end;

theorem Th6: :: ZF_FUND1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being Universe
for X being Subclass of V
for o, p being set st X is closed_wrt_A1-A7 & o in X & p in X holds
( {o,p} in X & [o,p] in X )
proof end;

theorem Th7: :: ZF_FUND1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being Universe
for X being Subclass of V st X is closed_wrt_A1-A7 holds
omega c= X
proof end;

theorem Th8: :: ZF_FUND1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being Universe
for X being Subclass of V
for fs being finite Subset of omega st X is closed_wrt_A1-A7 holds
Funcs fs,omega c= X
proof end;

theorem Th9: :: ZF_FUND1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being Universe
for a being Element of V
for X being Subclass of V
for fs being finite Subset of omega st X is closed_wrt_A1-A7 & a in X holds
Funcs fs,a in X
proof end;

theorem Th10: :: ZF_FUND1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being Universe
for a, b being Element of V
for X being Subclass of V
for fs being finite Subset of omega st X is closed_wrt_A1-A7 & a in Funcs fs,omega & b in X holds
{ (a (#) x) where x is Element of V : x in b } in X
proof end;

Lm13: for V being Universe
for X being Subclass of V
for n being Element of omega st X is closed_wrt_A1-A7 holds
n in X
proof end;

Lm14: for V being Universe
for X being Subclass of V st X is closed_wrt_A1-A7 holds
( 0-element_of V in X & 1-element_of V in X )
proof end;

theorem Th11: :: ZF_FUND1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being Universe
for a, b being Element of V
for X being Subclass of V
for n being Element of omega
for fs being finite Subset of omega st X is closed_wrt_A1-A7 & n in fs & a in X & b in X & b c= Funcs fs,a holds
{ x where x is Element of V : ( x in Funcs (fs \ {n}),a & ex u being set st {[n,u]} \/ x in b ) } in X
proof end;

theorem Th12: :: ZF_FUND1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being Universe
for a, b being Element of V
for X being Subclass of V
for n being Element of omega
for fs being finite Subset of omega st X is closed_wrt_A1-A7 & not n in fs & a in X & b in X & b c= Funcs fs,a holds
{ ({[n,x]} \/ y) where x, y is Element of V : ( x in a & y in b ) } in X
proof end;

theorem Th13: :: ZF_FUND1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being Universe
for X being Subclass of V
for B being set st X is closed_wrt_A1-A7 & B is finite & ( for o being set st o in B holds
o in X ) holds
B in X
proof end;

theorem Th14: :: ZF_FUND1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being Universe
for y being Element of V
for X being Subclass of V
for A being set
for fs being finite Subset of omega st X is closed_wrt_A1-A7 & A c= X & y in Funcs fs,A holds
y in X
proof end;

theorem Th15: :: ZF_FUND1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being Universe
for a, y being Element of V
for X being Subclass of V
for n being Element of omega
for fs being finite Subset of omega st X is closed_wrt_A1-A7 & not n in fs & a in X & a c= X & y in Funcs fs,a holds
{ ({[n,x]} \/ y) where x is Element of V : x in a } in X
proof end;

theorem :: ZF_FUND1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being Universe
for a, y, b being Element of V
for X being Subclass of V
for n being Element of omega
for fs being finite Subset of omega st X is closed_wrt_A1-A7 & not n in fs & a in X & a c= X & y in Funcs fs,a & b c= Funcs (fs \/ {n}),a & b in X holds
{ x where x is Element of V : ( x in a & {[n,x]} \/ y in b ) } in X
proof end;

Lm15: for o, p, q being set holds {[o,p],[p,p]} (#) {[p,q]} = {[o,q],[p,q]}
proof end;

theorem Th17: :: ZF_FUND1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being Universe
for a being Element of V
for X being Subclass of V st X is closed_wrt_A1-A7 & a in X holds
{ {[(0-element_of V),x],[(1-element_of V),x]} where x is Element of V : x in a } in X
proof end;

Lm16: for p, r, o, q, s, t being set st p <> r holds
{[o,p],[q,r]} (#) {[p,s],[r,t]} = {[o,s],[q,t]}
proof end;

Lm17: for o, q being set
for g being Function holds
( dom g = {o,q} iff g = {[o,(g . o)],[q,(g . q)]} )
proof end;

theorem Th18: :: ZF_FUND1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being Universe
for X being Subclass of V
for E being non empty set st X is closed_wrt_A1-A7 & E in X holds
for v1, v2 being Element of VAR holds
( Diagram (v1 '=' v2),E in X & Diagram (v1 'in' v2),E in X )
proof end;

theorem Th19: :: ZF_FUND1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being Universe
for X being Subclass of V
for E being non empty set st X is closed_wrt_A1-A7 & E in X holds
for H being ZF-formula st Diagram H,E in X holds
Diagram ('not' H),E in X
proof end;

theorem Th20: :: ZF_FUND1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being Universe
for X being Subclass of V
for E being non empty set st X is closed_wrt_A1-A7 & E in X holds
for H, H' being ZF-formula st Diagram H,E in X & Diagram H',E in X holds
Diagram (H '&' H'),E in X
proof end;

theorem Th21: :: ZF_FUND1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being Universe
for X being Subclass of V
for E being non empty set st X is closed_wrt_A1-A7 & E in X holds
for H being ZF-formula
for v1 being Element of VAR st Diagram H,E in X holds
Diagram (All v1,H),E in X
proof end;

theorem :: ZF_FUND1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being Universe
for X being Subclass of V
for E being non empty set
for H being ZF-formula st X is closed_wrt_A1-A7 & E in X holds
Diagram H,E in X
proof end;

theorem :: ZF_FUND1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being Universe
for X being Subclass of V
for n being Element of omega st X is closed_wrt_A1-A7 holds
( n in X & 0-element_of V in X & 1-element_of V in X ) by Lm13, Lm14;

theorem :: ZF_FUND1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for o, p, q being set holds {[o,p],[p,p]} (#) {[p,q]} = {[o,q],[p,q]} by Lm15;

theorem :: ZF_FUND1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, r, o, q, s, t being set st p <> r holds
{[o,p],[q,r]} (#) {[p,s],[r,t]} = {[o,s],[q,t]} by Lm16;

theorem :: ZF_FUND1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: ZF_FUND1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for v1, v2 being Element of VAR holds
( code {v1} = {(x". v1)} & code {v1,v2} = {(x". v1),(x". v2)} ) by Lm6, Lm7;

theorem :: ZF_FUND1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for o, q being set
for f being Function holds
( dom f = {o,q} iff f = {[o,(f . o)],[q,(f . q)]} ) by Lm17;

theorem :: ZF_FUND1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
( dom decode = omega & rng decode = VAR & decode is one-to-one & decode " is one-to-one & dom (decode " ) = VAR & rng (decode " ) = omega ) by Lm1;

theorem :: ZF_FUND1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being finite Subset of VAR holds A, code A are_equipotent by Lm8;

theorem :: ZF_FUND1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A being Element of omega holds A = x". (x. (card A)) by Lm2;

theorem :: ZF_FUND1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for fs being finite Subset of omega
for E being non empty set
for f being Function of VAR ,E holds
( dom ((f * decode ) | fs) = fs & rng ((f * decode ) | fs) c= E & (f * decode ) | fs in Funcs fs,E & dom (f * decode ) = omega & rng (f * decode ) c= E ) by Lm3;

theorem :: ZF_FUND1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty set
for f being Function of VAR ,E
for v1 being Element of VAR holds
( decode . (x". v1) = v1 & (decode " ) . v1 = x". v1 & (f * decode ) . (x". v1) = f . v1 ) by Lm4;

theorem :: ZF_FUND1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being set
for A being finite Subset of VAR holds
( p in code A iff ex v1 being Element of VAR st
( v1 in A & p = x". v1 ) ) by Lm5;

theorem :: ZF_FUND1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for A, B being finite Subset of VAR holds
( code (A \/ B) = (code A) \/ (code B) & code (A \ B) = (code A) \ (code B) ) by Lm9;

theorem :: ZF_FUND1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty set
for f being Function of VAR ,E
for v1 being Element of VAR
for H being ZF-formula st v1 in Free H holds
((f * decode ) | (code (Free H))) . (x". v1) = f . v1 by Lm10;

theorem :: ZF_FUND1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for E being non empty set
for H being ZF-formula
for f, g being Function of VAR ,E st (f * decode ) | (code (Free H)) = (g * decode ) | (code (Free H)) & f in St H,E holds
g in St H,E by Lm11;

theorem :: ZF_FUND1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being set
for fs being finite Subset of omega
for E being non empty set st p in Funcs fs,E holds
ex f being Function of VAR ,E st p = (f * decode ) | fs by Lm12;