:: ZF_FUND1 semantic presentation

definition
let c1, c2 be set ;
func c1 (#) c2 -> set means :Def1: :: ZF_FUND1:def 1
for b1 being set holds
( b1 in a3 iff ex b2, b3, b4 being set st
( b1 = [b2,b4] & [b2,b3] in a1 & [b3,b4] in a2 ) );
existence
ex b1 being set st
for b2 being set holds
( b2 in b1 iff ex b3, b4, b5 being set st
( b2 = [b3,b5] & [b3,b4] in c1 & [b4,b5] in c2 ) )
proof end;
uniqueness
for b1, b2 being set st ( for b3 being set holds
( b3 in b1 iff ex b4, b5, b6 being set st
( b3 = [b4,b6] & [b4,b5] in c1 & [b5,b6] in c2 ) ) ) & ( for b3 being set holds
( b3 in b2 iff ex b4, b5, b6 being set st
( b3 = [b4,b6] & [b4,b5] in c1 & [b5,b6] in c2 ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def1 defines (#) ZF_FUND1:def 1 :
for b1, b2, b3 being set holds
( b3 = b1 (#) b2 iff for b4 being set holds
( b4 in b3 iff ex b5, b6, b7 being set st
( b4 = [b5,b7] & [b5,b6] in b1 & [b6,b7] in b2 ) ) );

definition
let c1 be Universe;
let c2, c3 be Element of c1;
redefine func (#) as c2 (#) c3 -> Element of a1;
coherence
c2 (#) c3 is Element of c1
proof end;
end;

definition
func decode -> Function of omega , VAR means :Def2: :: ZF_FUND1:def 2
for b1 being Element of omega holds a1 . b1 = x. (card b1);
existence
ex b1 being Function of omega , VAR st
for b2 being Element of omega holds b1 . b2 = x. (card b2)
proof end;
uniqueness
for b1, b2 being Function of omega , VAR st ( for b3 being Element of omega holds b1 . b3 = x. (card b3) ) & ( for b3 being Element of omega holds b2 . b3 = x. (card b3) ) 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 b2 being Element of omega holds b1 . b2 = x. (card b2) );

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

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

Lemma4: ( 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 c1 be finite Subset of VAR ;
func code c1 -> finite Subset of omega equals :: ZF_FUND1:def 4
(decode " ) .: a1;
coherence
(decode " ) .: c1 is finite Subset of omega by Lemma4, RELAT_1:144;
end;

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

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

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

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

definition
let c1 be ZF-formula;
let c2 be non empty set ;
func Diagram c1,c2 -> set means :Def5: :: ZF_FUND1:def 5
for b1 being set holds
( b1 in a3 iff ex b2 being Function of VAR ,a2 st
( b1 = (b2 * decode ) | (code (Free a1)) & b2 in St a1,a2 ) );
existence
ex b1 being set st
for b2 being set holds
( b2 in b1 iff ex b3 being Function of VAR ,c2 st
( b2 = (b3 * decode ) | (code (Free c1)) & b3 in St c1,c2 ) )
proof end;
uniqueness
for b1, b2 being set st ( for b3 being set holds
( b3 in b1 iff ex b4 being Function of VAR ,c2 st
( b3 = (b4 * decode ) | (code (Free c1)) & b4 in St c1,c2 ) ) ) & ( for b3 being set holds
( b3 in b2 iff ex b4 being Function of VAR ,c2 st
( b3 = (b4 * decode ) | (code (Free c1)) & b4 in St c1,c2 ) ) ) holds
b1 = b2
proof end;
end;

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

definition
let c1 be Universe;
let c2 be Subclass of c1;
attr a2 is closed_wrt_A1 means :Def6: :: ZF_FUND1:def 6
for b1 being Element of a1 st b1 in a2 holds
{ {[(0-element_of a1),b2],[(1-element_of a1),b3]} where B is Element of a1, B is Element of a1 : ( b2 in b3 & b2 in b1 & b3 in b1 ) } in a2;
attr a2 is closed_wrt_A2 means :Def7: :: ZF_FUND1:def 7
for b1, b2 being Element of a1 st b1 in a2 & b2 in a2 holds
{b1,b2} in a2;
attr a2 is closed_wrt_A3 means :Def8: :: ZF_FUND1:def 8
for b1 being Element of a1 st b1 in a2 holds
union b1 in a2;
attr a2 is closed_wrt_A4 means :Def9: :: ZF_FUND1:def 9
for b1, b2 being Element of a1 st b1 in a2 & b2 in a2 holds
{ {[b3,b4]} where B is Element of a1, B is Element of a1 : ( b3 in b1 & b4 in b2 ) } in a2;
attr a2 is closed_wrt_A5 means :Def10: :: ZF_FUND1:def 10
for b1, b2 being Element of a1 st b1 in a2 & b2 in a2 holds
{ (b3 \/ b4) where B is Element of a1, B is Element of a1 : ( b3 in b1 & b4 in b2 ) } in a2;
attr a2 is closed_wrt_A6 means :Def11: :: ZF_FUND1:def 11
for b1, b2 being Element of a1 st b1 in a2 & b2 in a2 holds
{ (b3 \ b4) where B is Element of a1, B is Element of a1 : ( b3 in b1 & b4 in b2 ) } in a2;
attr a2 is closed_wrt_A7 means :Def12: :: ZF_FUND1:def 12
for b1, b2 being Element of a1 st b1 in a2 & b2 in a2 holds
{ (b3 (#) b4) where B is Element of a1, B is Element of a1 : ( b3 in b1 & b4 in b2 ) } in a2;
end;

:: deftheorem Def6 defines closed_wrt_A1 ZF_FUND1:def 6 :
for b1 being Universe
for b2 being Subclass of b1 holds
( b2 is closed_wrt_A1 iff for b3 being Element of b1 st b3 in b2 holds
{ {[(0-element_of b1),b4],[(1-element_of b1),b5]} where B is Element of b1, B is Element of b1 : ( b4 in b5 & b4 in b3 & b5 in b3 ) } in b2 );

:: deftheorem Def7 defines closed_wrt_A2 ZF_FUND1:def 7 :
for b1 being Universe
for b2 being Subclass of b1 holds
( b2 is closed_wrt_A2 iff for b3, b4 being Element of b1 st b3 in b2 & b4 in b2 holds
{b3,b4} in b2 );

:: deftheorem Def8 defines closed_wrt_A3 ZF_FUND1:def 8 :
for b1 being Universe
for b2 being Subclass of b1 holds
( b2 is closed_wrt_A3 iff for b3 being Element of b1 st b3 in b2 holds
union b3 in b2 );

:: deftheorem Def9 defines closed_wrt_A4 ZF_FUND1:def 9 :
for b1 being Universe
for b2 being Subclass of b1 holds
( b2 is closed_wrt_A4 iff for b3, b4 being Element of b1 st b3 in b2 & b4 in b2 holds
{ {[b5,b6]} where B is Element of b1, B is Element of b1 : ( b5 in b3 & b6 in b4 ) } in b2 );

:: deftheorem Def10 defines closed_wrt_A5 ZF_FUND1:def 10 :
for b1 being Universe
for b2 being Subclass of b1 holds
( b2 is closed_wrt_A5 iff for b3, b4 being Element of b1 st b3 in b2 & b4 in b2 holds
{ (b5 \/ b6) where B is Element of b1, B is Element of b1 : ( b5 in b3 & b6 in b4 ) } in b2 );

:: deftheorem Def11 defines closed_wrt_A6 ZF_FUND1:def 11 :
for b1 being Universe
for b2 being Subclass of b1 holds
( b2 is closed_wrt_A6 iff for b3, b4 being Element of b1 st b3 in b2 & b4 in b2 holds
{ (b5 \ b6) where B is Element of b1, B is Element of b1 : ( b5 in b3 & b6 in b4 ) } in b2 );

:: deftheorem Def12 defines closed_wrt_A7 ZF_FUND1:def 12 :
for b1 being Universe
for b2 being Subclass of b1 holds
( b2 is closed_wrt_A7 iff for b3, b4 being Element of b1 st b3 in b2 & b4 in b2 holds
{ (b5 (#) b6) where B is Element of b1, B is Element of b1 : ( b5 in b3 & b6 in b4 ) } in b2 );

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

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

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

Lemma15: for b1 being finite Subset of omega
for b2 being non empty set
for b3 being Function of VAR ,b2 holds
( dom ((b3 * decode ) | b1) = b1 & rng ((b3 * decode ) | b1) c= b2 & (b3 * decode ) | b1 in Funcs b1,b2 & dom (b3 * decode ) = omega & rng (b3 * decode ) c= b2 )
proof end;

Lemma16: for b1 being non empty set
for b2 being Function of VAR ,b1
for b3 being Element of VAR holds
( decode . (x". b3) = b3 & (decode " ) . b3 = x". b3 & (b2 * decode ) . (x". b3) = b2 . b3 )
proof end;

Lemma17: for b1 being set
for b2 being finite Subset of VAR holds
( b1 in code b2 iff ex b3 being Element of VAR st
( b3 in b2 & b1 = x". b3 ) )
proof end;

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

Lemma19: for b1, b2 being Element of VAR holds code {b1,b2} = {(x". b1),(x". b2)}
proof end;

Lemma20: for b1 being finite Subset of VAR holds b1, code b1 are_equipotent
proof end;

Lemma21: for b1, b2 being finite Subset of VAR holds
( code (b1 \/ b2) = (code b1) \/ (code b2) & code (b1 \ b2) = (code b1) \ (code b2) )
by RELAT_1:153, Lemma4, FUNCT_1:123;

Lemma22: for b1 being non empty set
for b2 being Function of VAR ,b1
for b3 being Element of VAR
for b4 being ZF-formula st b3 in Free b4 holds
((b2 * decode ) | (code (Free b4))) . (x". b3) = b2 . b3
proof end;

Lemma23: for b1 being non empty set
for b2 being ZF-formula
for b3, b4 being Function of VAR ,b1 st (b3 * decode ) | (code (Free b2)) = (b4 * decode ) | (code (Free b2)) & b3 in St b2,b1 holds
b4 in St b2,b1
proof end;

Lemma24: for b1 being set
for b2 being finite Subset of omega
for b3 being non empty set st b1 in Funcs b2,b3 holds
ex b4 being Function of VAR ,b3 st b1 = (b4 * decode ) | b2
proof end;

theorem Th1: :: ZF_FUND1:1
for b1 being Universe
for b2 being Subclass of b1
for b3, b4 being set holds
( b2 c= b1 & ( b3 in b2 implies b3 is Element of b1 ) & ( b3 in b4 & b4 in b2 implies b3 is Element of b1 ) )
proof end;

theorem Th2: :: ZF_FUND1:2
for b1 being Universe
for b2 being Subclass of b1
for b3, b4 being set st b2 is closed_wrt_A1-A7 holds
( ( b3 in b2 implies {b3} in b2 ) & ( {b3} in b2 implies b3 in b2 ) & ( b4 in b2 implies union b4 in b2 ) )
proof end;

theorem Th3: :: ZF_FUND1:3
for b1 being Universe
for b2 being Subclass of b1 st b2 is closed_wrt_A1-A7 holds
{} in b2
proof end;

theorem Th4: :: ZF_FUND1:4
for b1 being Universe
for b2 being Subclass of b1
for b3, b4 being set st b2 is closed_wrt_A1-A7 & b3 in b2 & b4 in b2 holds
( b3 \/ b4 in b2 & b3 \ b4 in b2 & b3 (#) b4 in b2 )
proof end;

theorem Th5: :: ZF_FUND1:5
for b1 being Universe
for b2 being Subclass of b1
for b3, b4 being set st b2 is closed_wrt_A1-A7 & b3 in b2 & b4 in b2 holds
b3 /\ b4 in b2
proof end;

theorem Th6: :: ZF_FUND1:6
for b1 being Universe
for b2 being Subclass of b1
for b3, b4 being set st b2 is closed_wrt_A1-A7 & b3 in b2 & b4 in b2 holds
( {b3,b4} in b2 & [b3,b4] in b2 )
proof end;

theorem Th7: :: ZF_FUND1:7
for b1 being Universe
for b2 being Subclass of b1 st b2 is closed_wrt_A1-A7 holds
omega c= b2
proof end;

theorem Th8: :: ZF_FUND1:8
for b1 being Universe
for b2 being Subclass of b1
for b3 being finite Subset of omega st b2 is closed_wrt_A1-A7 holds
Funcs b3,omega c= b2
proof end;

theorem Th9: :: ZF_FUND1:9
for b1 being Universe
for b2 being Element of b1
for b3 being Subclass of b1
for b4 being finite Subset of omega st b3 is closed_wrt_A1-A7 & b2 in b3 holds
Funcs b4,b2 in b3
proof end;

theorem Th10: :: ZF_FUND1:10
for b1 being Universe
for b2, b3 being Element of b1
for b4 being Subclass of b1
for b5 being finite Subset of omega st b4 is closed_wrt_A1-A7 & b2 in Funcs b5,omega & b3 in b4 holds
{ (b2 (#) b6) where B is Element of b1 : b6 in b3 } in b4
proof end;

Lemma35: for b1 being Universe
for b2 being Subclass of b1
for b3 being Element of omega st b2 is closed_wrt_A1-A7 holds
b3 in b2
proof end;

Lemma36: for b1 being Universe
for b2 being Subclass of b1 st b2 is closed_wrt_A1-A7 holds
( 0-element_of b1 in b2 & 1-element_of b1 in b2 )
proof end;

theorem Th11: :: ZF_FUND1:11
for b1 being Universe
for b2, b3 being Element of b1
for b4 being Subclass of b1
for b5 being Element of omega
for b6 being finite Subset of omega st b4 is closed_wrt_A1-A7 & b5 in b6 & b2 in b4 & b3 in b4 & b3 c= Funcs b6,b2 holds
{ b7 where B is Element of b1 : ( b7 in Funcs (b6 \ {b5}),b2 & ex b1 being set st {[b5,b8]} \/ b7 in b3 ) } in b4
proof end;

theorem Th12: :: ZF_FUND1:12
for b1 being Universe
for b2, b3 being Element of b1
for b4 being Subclass of b1
for b5 being Element of omega
for b6 being finite Subset of omega st b4 is closed_wrt_A1-A7 & not b5 in b6 & b2 in b4 & b3 in b4 & b3 c= Funcs b6,b2 holds
{ ({[b5,b7]} \/ b8) where B is Element of b1, B is Element of b1 : ( b7 in b2 & b8 in b3 ) } in b4
proof end;

theorem Th13: :: ZF_FUND1:13
for b1 being Universe
for b2 being Subclass of b1
for b3 being set st b2 is closed_wrt_A1-A7 & b3 is finite & ( for b4 being set st b4 in b3 holds
b4 in b2 ) holds
b3 in b2
proof end;

theorem Th14: :: ZF_FUND1:14
for b1 being Universe
for b2 being Element of b1
for b3 being Subclass of b1
for b4 being set
for b5 being finite Subset of omega st b3 is closed_wrt_A1-A7 & b4 c= b3 & b2 in Funcs b5,b4 holds
b2 in b3
proof end;

theorem Th15: :: ZF_FUND1:15
for b1 being Universe
for b2, b3 being Element of b1
for b4 being Subclass of b1
for b5 being Element of omega
for b6 being finite Subset of omega st b4 is closed_wrt_A1-A7 & not b5 in b6 & b2 in b4 & b2 c= b4 & b3 in Funcs b6,b2 holds
{ ({[b5,b7]} \/ b3) where B is Element of b1 : b7 in b2 } in b4
proof end;

theorem Th16: :: ZF_FUND1:16
for b1 being Universe
for b2, b3, b4 being Element of b1
for b5 being Subclass of b1
for b6 being Element of omega
for b7 being finite Subset of omega st b5 is closed_wrt_A1-A7 & not b6 in b7 & b2 in b5 & b2 c= b5 & b3 in Funcs b7,b2 & b4 c= Funcs (b7 \/ {b6}),b2 & b4 in b5 holds
{ b8 where B is Element of b1 : ( b8 in b2 & {[b6,b8]} \/ b3 in b4 ) } in b5
proof end;

Lemma42: for b1, b2, b3 being set holds {[b1,b2],[b2,b2]} (#) {[b2,b3]} = {[b1,b3],[b2,b3]}
proof end;

theorem Th17: :: ZF_FUND1:17
for b1 being Universe
for b2 being Element of b1
for b3 being Subclass of b1 st b3 is closed_wrt_A1-A7 & b2 in b3 holds
{ {[(0-element_of b1),b4],[(1-element_of b1),b4]} where B is Element of b1 : b4 in b2 } in b3
proof end;

Lemma44: for b1, b2, b3, b4, b5, b6 being set st b1 <> b2 holds
{[b3,b1],[b4,b2]} (#) {[b1,b5],[b2,b6]} = {[b3,b5],[b4,b6]}
proof end;

Lemma45: for b1, b2 being set
for b3 being Function holds
( dom b3 = {b1,b2} iff b3 = {[b1,(b3 . b1)],[b2,(b3 . b2)]} )
proof end;

theorem Th18: :: ZF_FUND1:18
for b1 being Universe
for b2 being Subclass of b1
for b3 being non empty set st b2 is closed_wrt_A1-A7 & b3 in b2 holds
for b4, b5 being Element of VAR holds
( Diagram (b4 '=' b5),b3 in b2 & Diagram (b4 'in' b5),b3 in b2 )
proof end;

theorem Th19: :: ZF_FUND1:19
for b1 being Universe
for b2 being Subclass of b1
for b3 being non empty set st b2 is closed_wrt_A1-A7 & b3 in b2 holds
for b4 being ZF-formula st Diagram b4,b3 in b2 holds
Diagram ('not' b4),b3 in b2
proof end;

theorem Th20: :: ZF_FUND1:20
for b1 being Universe
for b2 being Subclass of b1
for b3 being non empty set st b2 is closed_wrt_A1-A7 & b3 in b2 holds
for b4, b5 being ZF-formula st Diagram b4,b3 in b2 & Diagram b5,b3 in b2 holds
Diagram (b4 '&' b5),b3 in b2
proof end;

theorem Th21: :: ZF_FUND1:21
for b1 being Universe
for b2 being Subclass of b1
for b3 being non empty set st b2 is closed_wrt_A1-A7 & b3 in b2 holds
for b4 being ZF-formula
for b5 being Element of VAR st Diagram b4,b3 in b2 holds
Diagram (All b5,b4),b3 in b2
proof end;

theorem Th22: :: ZF_FUND1:22
for b1 being Universe
for b2 being Subclass of b1
for b3 being non empty set
for b4 being ZF-formula st b2 is closed_wrt_A1-A7 & b3 in b2 holds
Diagram b4,b3 in b2
proof end;

theorem Th23: :: ZF_FUND1:23
for b1 being Universe
for b2 being Subclass of b1
for b3 being Element of omega st b2 is closed_wrt_A1-A7 holds
( b3 in b2 & 0-element_of b1 in b2 & 1-element_of b1 in b2 ) by Lemma35, Lemma36;

theorem Th24: :: ZF_FUND1:24
for b1, b2, b3 being set holds {[b1,b2],[b2,b2]} (#) {[b2,b3]} = {[b1,b3],[b2,b3]} by Lemma42;

theorem Th25: :: ZF_FUND1:25
for b1, b2, b3, b4, b5, b6 being set st b1 <> b2 holds
{[b3,b1],[b4,b2]} (#) {[b1,b5],[b2,b6]} = {[b3,b5],[b4,b6]} by Lemma44;

theorem Th26: :: ZF_FUND1:26
canceled;

theorem Th27: :: ZF_FUND1:27
for b1, b2 being Element of VAR holds
( code {b1} = {(x". b1)} & code {b1,b2} = {(x". b1),(x". b2)} ) by Lemma18, Lemma19;

theorem Th28: :: ZF_FUND1:28
for b1, b2 being set
for b3 being Function holds
( dom b3 = {b1,b2} iff b3 = {[b1,(b3 . b1)],[b2,(b3 . b2)]} ) by Lemma45;

theorem Th29: :: ZF_FUND1:29
( dom decode = omega & rng decode = VAR & decode is one-to-one & decode " is one-to-one & dom (decode " ) = VAR & rng (decode " ) = omega ) by Lemma4;

theorem Th30: :: ZF_FUND1:30
for b1 being finite Subset of VAR holds b1, code b1 are_equipotent by Lemma20;

theorem Th31: :: ZF_FUND1:31
for b1 being Element of omega holds b1 = x". (x. (card b1)) by Lemma14;

theorem Th32: :: ZF_FUND1:32
for b1 being finite Subset of omega
for b2 being non empty set
for b3 being Function of VAR ,b2 holds
( dom ((b3 * decode ) | b1) = b1 & rng ((b3 * decode ) | b1) c= b2 & (b3 * decode ) | b1 in Funcs b1,b2 & dom (b3 * decode ) = omega & rng (b3 * decode ) c= b2 ) by Lemma15;

theorem Th33: :: ZF_FUND1:33
for b1 being non empty set
for b2 being Function of VAR ,b1
for b3 being Element of VAR holds
( decode . (x". b3) = b3 & (decode " ) . b3 = x". b3 & (b2 * decode ) . (x". b3) = b2 . b3 ) by Lemma16;

theorem Th34: :: ZF_FUND1:34
for b1 being set
for b2 being finite Subset of VAR holds
( b1 in code b2 iff ex b3 being Element of VAR st
( b3 in b2 & b1 = x". b3 ) ) by Lemma17;

theorem Th35: :: ZF_FUND1:35
for b1, b2 being finite Subset of VAR holds
( code (b1 \/ b2) = (code b1) \/ (code b2) & code (b1 \ b2) = (code b1) \ (code b2) ) by Lemma21;

theorem Th36: :: ZF_FUND1:36
for b1 being non empty set
for b2 being Function of VAR ,b1
for b3 being Element of VAR
for b4 being ZF-formula st b3 in Free b4 holds
((b2 * decode ) | (code (Free b4))) . (x". b3) = b2 . b3 by Lemma22;

theorem Th37: :: ZF_FUND1:37
for b1 being non empty set
for b2 being ZF-formula
for b3, b4 being Function of VAR ,b1 st (b3 * decode ) | (code (Free b2)) = (b4 * decode ) | (code (Free b2)) & b3 in St b2,b1 holds
b4 in St b2,b1 by Lemma23;

theorem Th38: :: ZF_FUND1:38
for b1 being set
for b2 being finite Subset of omega
for b3 being non empty set st b1 in Funcs b2,b3 holds
ex b4 being Function of VAR ,b3 st b1 = (b4 * decode ) | b2 by Lemma24;