:: FRAENKEL semantic presentation

scheme :: FRAENKEL:sch 1
s1{ F1() -> non empty set , F2( set ) -> set , P1[ set ], P2[ set ] } :
{ F2(b1) where B is Element of F1() : P1[b1] } c= { F2(b1) where B is Element of F1() : P2[b1] }
provided
E1: for b1 being Element of F1() st P1[b1] holds
P2[b1]
proof end;

scheme :: FRAENKEL:sch 2
s2{ F1() -> non empty set , F2() -> non empty set , F3( set , set ) -> set , P1[ set , set ], P2[ set , set ] } :
{ F3(b1,b2) where B is Element of F1(), B is Element of F2() : P1[b1,b2] } c= { F3(b1,b2) where B is Element of F1(), B is Element of F2() : P2[b1,b2] }
provided
E1: for b1 being Element of F1()
for b2 being Element of F2() st P1[b1,b2] holds
P2[b1,b2]
proof end;

scheme :: FRAENKEL:sch 3
s3{ F1() -> non empty set , F2( set ) -> set , P1[ set ], P2[ set ] } :
{ F2(b1) where B is Element of F1() : P1[b1] } = { F2(b1) where B is Element of F1() : P2[b1] }
provided
E1: for b1 being Element of F1() holds
( P1[b1] iff P2[b1] )
proof end;

scheme :: FRAENKEL:sch 4
s4{ F1() -> non empty set , F2() -> non empty set , F3( set , set ) -> set , P1[ set , set ], P2[ set , set ] } :
{ F3(b1,b2) where B is Element of F1(), B is Element of F2() : P1[b1,b2] } = { F3(b1,b2) where B is Element of F1(), B is Element of F2() : P2[b1,b2] }
provided
E1: for b1 being Element of F1()
for b2 being Element of F2() holds
( P1[b1,b2] iff P2[b1,b2] )
proof end;

scheme :: FRAENKEL:sch 5
s5{ F1() -> non empty set , F2( set ) -> set , F3( set ) -> set , P1[ set ] } :
{ F2(b1) where B is Element of F1() : P1[b1] } = { F3(b1) where B is Element of F1() : P1[b1] }
provided
E1: for b1 being Element of F1() holds F2(b1) = F3(b1)
proof end;

scheme :: FRAENKEL:sch 6
s6{ F1() -> non empty set , F2( set ) -> set , F3( set ) -> set , P1[ set ] } :
{ F2(b1) where B is Element of F1() : P1[b1] } = { F3(b1) where B is Element of F1() : P1[b1] }
provided
E1: for b1 being Element of F1() st P1[b1] holds
F2(b1) = F3(b1)
proof end;

scheme :: FRAENKEL:sch 7
s7{ F1() -> non empty set , F2() -> non empty set , F3( set , set ) -> set , F4( set , set ) -> set , P1[ set , set ] } :
{ F3(b1,b2) where B is Element of F1(), B is Element of F2() : P1[b1,b2] } = { F4(b1,b2) where B is Element of F1(), B is Element of F2() : P1[b1,b2] }
provided
E1: for b1 being Element of F1()
for b2 being Element of F2() holds F3(b1,b2) = F4(b1,b2)
proof end;

scheme :: FRAENKEL:sch 8
s8{ F1() -> non empty set , F2() -> non empty set , F3( set , set ) -> set , P1[ set , set ], P2[ set , set ] } :
{ F3(b1,b2) where B is Element of F1(), B is Element of F2() : P1[b1,b2] } = { F3(b2,b1) where B is Element of F1(), B is Element of F2() : P2[b1,b2] }
provided
E1: for b1 being Element of F1()
for b2 being Element of F2() holds
( P1[b1,b2] iff P2[b1,b2] ) and
E2: for b1 being Element of F1()
for b2 being Element of F2() holds F3(b1,b2) = F3(b2,b1)
proof end;

theorem Th1: :: FRAENKEL:1
canceled;

theorem Th2: :: FRAENKEL:2
canceled;

theorem Th3: :: FRAENKEL:3
for b1, b2 being non empty set
for b3, b4 being Function of b1,b2
for b5 being set st b3 | b5 = b4 | b5 holds
for b6 being Element of b1 st b6 in b5 holds
b3 . b6 = b4 . b6
proof end;

theorem Th4: :: FRAENKEL:4
canceled;

theorem Th5: :: FRAENKEL:5
for b1, b2 being set holds Funcs b1,b2 c= bool [:b1,b2:]
proof end;

theorem Th6: :: FRAENKEL:6
for b1 being non empty set
for b2, b3, b4 being set st Funcs b3,b4 <> {} & b3 c= b2 & b4 c= b1 holds
for b5 being Element of Funcs b3,b4 holds b5 is PartFunc of b2,b1
proof end;

scheme :: FRAENKEL:sch 9
s9{ F1() -> non empty set , F2() -> non empty set , F3() -> set , F4() -> Function of F1(),F2(), F5() -> Function of F1(),F2(), P1[ set ], P2[ set ] } :
{ (F4() . b1) where B is Element of F1() : ( P1[b1] & b1 in F3() ) } = { (F5() . b1) where B is Element of F1() : ( P2[b1] & b1 in F3() ) }
provided
E4: F4() | F3() = F5() | F3() and
E5: for b1 being Element of F1() st b1 in F3() holds
( P1[b1] iff P2[b1] )
proof end;

scheme :: FRAENKEL:sch 10
s10{ F1() -> non empty set , P1[ set ] } :
{ b1 where B is Element of F1() : P1[b1] } c= F1()
proof end;

scheme :: FRAENKEL:sch 11
s11{ F1() -> non empty set , F2() -> non empty set , F3( set , set ) -> set , P1[ set , set ], P2[ set ] } :
for b1 being Element of F1()
for b2 being Element of F2() st P1[b1,b2] holds
P2[F3(b1,b2)]
provided
E4: for b1 being set st b1 in { F3(b2,b3) where B is Element of F1(), B is Element of F2() : P1[b2,b3] } holds
P2[b1]
proof end;

scheme :: FRAENKEL:sch 12
s12{ F1() -> non empty set , F2() -> non empty set , F3( set , set ) -> set , P1[ set , set ], P2[ set ] } :
for b1 being set st b1 in { F3(b2,b3) where B is Element of F1(), B is Element of F2() : P1[b2,b3] } holds
P2[b1]
provided
E4: for b1 being Element of F1()
for b2 being Element of F2() st P1[b1,b2] holds
P2[F3(b1,b2)]
proof end;

scheme :: FRAENKEL:sch 13
s13{ F1() -> non empty set , F2() -> non empty set , F3() -> non empty set , F4( set , set ) -> Element of F3(), P1[ set , set ], P2[ set ] } :
{ b1 where B is Element of F3() : ( b1 in { F4(b2,b3) where B is Element of F1(), B is Element of F2() : P1[b2,b3] } & P2[b1] ) } = { F4(b1,b2) where B is Element of F1(), B is Element of F2() : ( P1[b1,b2] & P2[F4(b1,b2)] ) }
proof end;

scheme :: FRAENKEL:sch 14
s14{ F1() -> non empty set , F2( set ) -> set , P1[ set ], P2[ set ] } :
{ F2(b1) where B is Element of F1() : ( b1 in { b2 where B is Element of F1() : P2[b2] } & P1[b1] ) } = { F2(b1) where B is Element of F1() : ( P2[b1] & P1[b1] ) }
proof end;

scheme :: FRAENKEL:sch 15
s15{ F1() -> non empty set , F2() -> non empty set , F3( set , set ) -> set , P1[ set , set ], P2[ set ] } :
{ F3(b1,b2) where B is Element of F1(), B is Element of F2() : ( b1 in { b3 where B is Element of F1() : P2[b3] } & P1[b1,b2] ) } = { F3(b1,b2) where B is Element of F1(), B is Element of F2() : ( P2[b1] & P1[b1,b2] ) }
proof end;

scheme :: FRAENKEL:sch 16
s16{ F1() -> non empty set , F2() -> non empty set , F3( set , set ) -> set , P1[ set , set ], P2[ set , set ] } :
{ F3(b1,b2) where B is Element of F1(), B is Element of F2() : P1[b1,b2] } c= { F3(b1,b2) where B is Element of F1(), B is Element of F2() : P2[b1,b2] }
provided
E4: for b1 being Element of F1()
for b2 being Element of F2() st P1[b1,b2] holds
ex b3 being Element of F1() st
( P2[b3,b2] & F3(b1,b2) = F3(b3,b2) )
proof end;

scheme :: FRAENKEL:sch 17
s17{ F1() -> non empty set , F2() -> set , P1[ set ], F3( set ) -> set } :
{ F3(b1) where B is Element of F1() : ( F3(b1) in F2() & P1[b1] ) } c= F2()
proof end;

scheme :: FRAENKEL:sch 18
s18{ F1() -> non empty set , F2() -> set , P1[ set ], F3( set ) -> set } :
{ F3(b1) where B is Element of F1() : ( P1[b1] & not F3(b1) in F2() ) } misses F2()
proof end;

scheme :: FRAENKEL:sch 19
s19{ F1() -> non empty set , F2() -> non empty set , F3( set , set ) -> set , F4() -> Element of F2(), P1[ set , set ], P2[ set , set ] } :
{ F3(b1,b2) where B is Element of F1(), B is Element of F2() : P2[b1,b2] } = { F3(b1,F4()) where B is Element of F1() : P1[b1,F4()] }
provided
E4: for b1 being Element of F1()
for b2 being Element of F2() holds
( P2[b1,b2] iff ( b2 = F4() & P1[b1,b2] ) )
proof end;

scheme :: FRAENKEL:sch 20
s20{ F1() -> non empty set , F2() -> non empty set , F3( set , set ) -> set , F4() -> Element of F2(), P1[ set , set ] } :
{ F3(b1,b2) where B is Element of F1(), B is Element of F2() : ( b2 = F4() & P1[b1,b2] ) } = { F3(b1,F4()) where B is Element of F1() : P1[b1,F4()] }
proof end;

definition
let c1 be set ;
attr a1 is functional means :Def1: :: FRAENKEL:def 1
for b1 being set st b1 in a1 holds
b1 is Function;
end;

:: deftheorem Def1 defines functional FRAENKEL:def 1 :
for b1 being set holds
( b1 is functional iff for b2 being set st b2 in b1 holds
b2 is Function );

registration
cluster non empty functional set ;
existence
ex b1 being set st
( not b1 is empty & b1 is functional )
proof end;
end;

registration
let c1 be functional set ;
cluster -> Relation-like Function-like Element of a1;
coherence
for b1 being Element of c1 holds
( b1 is Function-like & b1 is Relation-like )
proof end;
end;

theorem Th7: :: FRAENKEL:7
canceled;

theorem Th8: :: FRAENKEL:8
for b1 being Function holds {b1} is functional
proof end;

registration
let c1, c2 be set ;
cluster Funcs a1,a2 -> functional ;
coherence
Funcs c1,c2 is functional
proof end;
end;

definition
let c1, c2 be set ;
mode FUNCTION_DOMAIN of c1,c2 -> non empty functional set means :Def2: :: FRAENKEL:def 2
for b1 being Element of a3 holds b1 is Function of a1,a2;
correctness
existence
ex b1 being non empty functional set st
for b2 being Element of b1 holds b2 is Function of c1,c2;
proof end;
end;

:: deftheorem Def2 defines FUNCTION_DOMAIN FRAENKEL:def 2 :
for b1, b2 being set
for b3 being non empty functional set holds
( b3 is FUNCTION_DOMAIN of b1,b2 iff for b4 being Element of b3 holds b4 is Function of b1,b2 );

theorem Th9: :: FRAENKEL:9
canceled;

theorem Th10: :: FRAENKEL:10
for b1, b2 being set
for b3 being Function of b1,b2 holds {b3} is FUNCTION_DOMAIN of b1,b2
proof end;

theorem Th11: :: FRAENKEL:11
for b1 being non empty set
for b2 being set holds Funcs b2,b1 is FUNCTION_DOMAIN of b2,b1
proof end;

definition
let c1 be set ;
let c2 be non empty set ;
redefine func Funcs as Funcs c1,c2 -> FUNCTION_DOMAIN of a1,a2;
coherence
Funcs c1,c2 is FUNCTION_DOMAIN of c1,c2 by Th11;
let c3 be FUNCTION_DOMAIN of c1,c2;
redefine mode Element as Element of c3 -> Function of a1,a2;
coherence
for b1 being Element of c3 holds b1 is Function of c1,c2 by Def2;
end;

theorem Th12: :: FRAENKEL:12
canceled;

theorem Th13: :: FRAENKEL:13
canceled;

theorem Th14: :: FRAENKEL:14
for b1 being non empty set
for b2, b3, b4 being set st Funcs b3,b4 <> {} & b3 c= b2 & b4 c= b1 holds
for b5 being Element of Funcs b3,b4 ex b6 being Element of Funcs b2,b1 st b6 | b3 = b5
proof end;

theorem Th15: :: FRAENKEL:15
for b1 being non empty set
for b2, b3 being set
for b4 being Element of Funcs b2,b1 holds b4 | b3 = b4 | (b2 /\ b3)
proof end;

scheme :: FRAENKEL:sch 21
s21{ F1() -> non empty set , F2() -> set , F3( set ) -> set } :
{ F3(b1) where B is Element of F1() : b1 in F2() } is finite
provided
E10: F2() is finite
proof end;

scheme :: FRAENKEL:sch 22
s22{ F1() -> non empty set , F2() -> non empty set , F3() -> set , F4() -> set , F5( set , set ) -> set } :
{ F5(b1,b2) where B is Element of F1(), B is Element of F2() : ( b1 in F3() & b2 in F4() ) } is finite
provided
E10: F3() is finite and
E11: F4() is finite
proof end;

scheme :: FRAENKEL:sch 23
s23{ F1() -> non empty set , F2() -> Element of Fin F1(), P1[ Element of F1(), Element of F1()] } :
for b1 being Element of F1() st b1 in F2() holds
ex b2 being Element of F1() st
( b2 in F2() & P1[b2,b1] & ( for b3 being Element of F1() st b3 in F2() & P1[b3,b2] holds
P1[b2,b3] ) )
provided
E10: for b1 being Element of F1() holds P1[b1,b1] and
E11: for b1, b2, b3 being Element of F1() st P1[b1,b2] & P1[b2,b3] holds
P1[b1,b3]
proof end;

scheme :: FRAENKEL:sch 24
s24{ F1() -> non empty set , F2() -> non empty set , F3() -> Element of Fin F2(), F4( set ) -> Element of F1(), P1[ set , set ] } :
ex b1 being Element of Fin F1() st
for b2 being Element of F1() holds
( b2 in b1 iff ex b3 being Element of F2() st
( b3 in F3() & b2 = F4(b3) & P1[b2,b3] ) )
proof end;

theorem Th16: :: FRAENKEL:16
for b1, b2 being set st b1 is finite & b2 is finite holds
Funcs b1,b2 is finite
proof end;

registration
let c1, c2 be finite set ;
cluster Funcs a1,a2 -> finite functional ;
coherence
Funcs c1,c2 is finite by Th16;
end;

scheme :: FRAENKEL:sch 25
s25{ F1() -> non empty set , F2() -> non empty set , F3() -> set , F4() -> set , F5( set ) -> set } :
{ F5(b1) where B is Element of Funcs F1(),F2() : b1 .: F3() c= F4() } is finite
provided
E11: F3() is finite and
E12: F4() is finite and
E13: for b1, b2 being Element of Funcs F1(),F2() st b1 | F3() = b2 | F3() holds
F5(b1) = F5(b2)
proof end;

scheme :: FRAENKEL:sch 26
s26{ F1() -> non empty set , F2() -> non empty set , P1[ Element of F1(), Element of F2()], F3() -> Element of Fin F1() } :
ex b1 being Function of F1(),F2() st
for b2 being Element of F1() st b2 in F3() holds
P1[b2,b1 . b2]
provided
E11: for b1 being Element of F1() st b1 in F3() holds
ex b2 being Element of F2() st P1[b1,b2]
proof end;

scheme :: FRAENKEL:sch 27
s27{ F1() -> non empty set , F2() -> non empty set , P1[ Element of F1(), Element of F2()], F3() -> Element of Fin F1() } :
ex b1 being Element of Funcs F1(),F2() st
for b2 being Element of F1() st b2 in F3() holds
P1[b2,b1 . b2]
provided
E11: for b1 being Element of F1() st b1 in F3() holds
ex b2 being Element of F2() st P1[b1,b2]
proof end;

theorem Th17: :: FRAENKEL:17
for b1 being functional set
for b2 being set st b2 c= b1 holds
b2 is functional
proof end;