:: YELLOW_3 semantic presentation

scheme :: YELLOW_3:sch 1
s1{ F₁() -> non empty set , F₂( set , set ) -> set , P₁[ set , set ], P₂[ set , set ] } :

{ F₂(b₁,b₂) where B is Element of F₁(), B is Element of F₁() : P₁[b₁,b₂] } is Subset of F₁()

provided

E1: for b₁, b₂ being Element of F₁() holds F₂(b₁,b₂) in F₁()

proof end;

scheme :: YELLOW_3:sch 2
s2{ F₁() -> Relation, F₂() -> Relation, P₁[ set , set ] } :

F₁() = F₂()

provided

E1: for b₁, b₂ being set holds
( [b₁,b₂] in F₁() iff P₁[b₁,b₂] ) and
E2: for b₁, b₂ being set holds
( [b₁,b₂] in F₂() iff P₁[b₁,b₂] )

proof end;

registration

let c₁ be empty set ;
cluster proj1 a₁ -> empty ;
coherence by FUNCT_5:10;
cluster proj2 a₁ -> empty ;
coherence by FUNCT_5:10;

end;

registration

let c₁, c₂ be non empty set ;
let c₃ be non empty Subset of [:c₁,c₂:];
cluster proj1 a₃ -> non empty ;
coherence

proof end;

cluster proj2 a₃ -> non empty ;
coherence

proof end;

end;

registration

let c₁ be RelStr ;
let c₂ be empty Subset of c₁;
cluster downarrow a₂ -> empty ;
coherence

proof end;

cluster uparrow a₂ -> empty ;
coherence

proof end;

end;

theorem Th1: :: YELLOW_3:1

for b₁, b₂ being set
for b₃ being Subset of [:b₁,b₂:] holds b₃ c= [:(proj1 b₃),(proj2 b₃):]

proof end;

Lemma2: for b₁, b₂, b₃, b₄, b₅ being set st b₁ = [[b₂,b₃],[b₄,b₅]] holds
( (b₁ `1 ) `1 = b₂ & (b₁ `1 ) `2 = b₃ & (b₁ `2 ) `1 = b₄ & (b₁ `2 ) `2 = b₅ )

proof end;

theorem Th2: :: YELLOW_3:2

for b₁ being transitive antisymmetric with_infima RelStr
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂ <= b₄ & b₃ <= b₅ holds
b₂ "/\" b₃ <= b₄ "/\" b₅

proof end;

theorem Th3: :: YELLOW_3:3

for b₁ being transitive antisymmetric with_suprema RelStr
for b₂, b₃, b₄, b₅ being Element of b₁ st b₂ <= b₄ & b₃ <= b₅ holds
b₂ "\/" b₃ <= b₄ "\/" b₅

proof end;

theorem Th4: :: YELLOW_3:4

for b₁ being non empty reflexive antisymmetric complete RelStr
for b₂ being Subset of b₁
for b₃ being Element of b₁ st b₃ in b₂ holds
(sup b₂) "/\" b₃ = b₃

proof end;

theorem Th5: :: YELLOW_3:5

for b₁ being non empty reflexive antisymmetric complete RelStr
for b₂ being Subset of b₁
for b₃ being Element of b₁ st b₃ in b₂ holds
(inf b₂) "\/" b₃ = b₃

proof end;

theorem Th6: :: YELLOW_3:6

for b₁ being RelStr
for b₂, b₃ being Subset of b₁ st b₂ c= b₃ holds
downarrow b₂ c= downarrow b₃

proof end;

theorem Th7: :: YELLOW_3:7

for b₁ being RelStr
for b₂, b₃ being Subset of b₁ st b₂ c= b₃ holds
uparrow b₂ c= uparrow b₃

proof end;

theorem Th8: :: YELLOW_3:8

for b₁, b₂ being with_infima Poset
for b₃ being Function of b₁,b₂
for b₄, b₅ being Element of b₁ holds
( b₃ preserves_inf_of {b₄,b₅} iff b₃ . (b₄ "/\" b₅) = (b₃ . b₄) "/\" (b₃ . b₅) )

proof end;

theorem Th9: :: YELLOW_3:9

for b₁, b₂ being with_suprema Poset
for b₃ being Function of b₁,b₂
for b₄, b₅ being Element of b₁ holds
( b₃ preserves_sup_of {b₄,b₅} iff b₃ . (b₄ "\/" b₅) = (b₃ . b₄) "\/" (b₃ . b₅) )

proof end;

scheme :: YELLOW_3:sch 3
s3{ F₁() -> non empty antisymmetric complete RelStr , P₁[ set ] } :

"/\" { ("/\" b₁,F₁()) where B is Subset of F₁() : P₁[b₁] } ,F₁() >= "/\" (union { b₁ where B is Subset of F₁() : P₁[b₁] } ),F₁()

proof end;

scheme :: YELLOW_3:sch 4
s4{ F₁() -> complete LATTICE, P₁[ set ] } :

"/\" { ("/\" b₁,F₁()) where B is Subset of F₁() : P₁[b₁] } ,F₁() = "/\" (union { b₁ where B is Subset of F₁() : P₁[b₁] } ),F₁()

proof end;

scheme :: YELLOW_3:sch 5
s5{ F₁() -> non empty antisymmetric complete RelStr , P₁[ set ] } :

"\/" { ("\/" b₁,F₁()) where B is Subset of F₁() : P₁[b₁] } ,F₁() <= "\/" (union { b₁ where B is Subset of F₁() : P₁[b₁] } ),F₁()

proof end;

scheme :: YELLOW_3:sch 6
s6{ F₁() -> complete LATTICE, P₁[ set ] } :

"\/" { ("\/" b₁,F₁()) where B is Subset of F₁() : P₁[b₁] } ,F₁() = "\/" (union { b₁ where B is Subset of F₁() : P₁[b₁] } ),F₁()

proof end;

definition

let c₁, c₂ be Relation;
func ["c₁,c₂"] -> Relation means :Def1: :: YELLOW_3:def 1
for b₁, b₂ being set holds
( [b₁,b₂] in a₃ iff ex b₃, b₄, b₅, b₆ being set st
( b₁ = [b₃,b₄] & b₂ = [b₅,b₆] & [b₃,b₅] in a₁ & [b₄,b₆] in a₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines [" YELLOW_3:def 1 :

theorem Th10: :: YELLOW_3:10

for b₁, b₂ being Relation
for b₃ being set holds
( b₃ in ["b₁,b₂"] iff ( [((b₃ `1 ) `1 ),((b₃ `2 ) `1 )] in b₁ & [((b₃ `1 ) `2 ),((b₃ `2 ) `2 )] in b₂ & ex b₄, b₅ being set st b₃ = [b₄,b₅] & ex b₄, b₅ being set st b₃ `1 = [b₄,b₅] & ex b₄, b₅ being set st b₃ `2 = [b₄,b₅] ) )

proof end;

definition

let c₁, c₂, c₃, c₄ be set ;
let c₅ be Relation of c₁,c₂;
let c₆ be Relation of c₃,c₄;
redefine func [" as ["c₅,c₆"] -> Relation of [:a₁,a₃:],[:a₂,a₄:];
coherence

proof end;

end;

definition

let c₁, c₂ be RelStr ;
func [:c₁,c₂:] -> strict RelStr means :Def2: :: YELLOW_3:def 2
( the carrier of a₃ = [:the carrier of a₁,the carrier of a₂:] & the InternalRel of a₃ = ["the InternalRel of a₁,the InternalRel of a₂"] );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def2 defines [: YELLOW_3:def 2 :

definition

let c₁, c₂ be RelStr ;
let c₃ be Subset of [:c₁,c₂:];
redefine func proj1 as proj1 c₃ -> Subset of a₁;
coherence

proof end;

redefine func proj2 as proj2 c₃ -> Subset of a₂;
coherence

proof end;

end;

definition

let c₁, c₂ be RelStr ;
let c₃ be Subset of c₁;
let c₄ be Subset of c₂;
redefine func [: as [:c₃,c₄:] -> Subset of [:a₁,a₂:];
coherence

proof end;

end;

definition

let c₁, c₂ be non empty RelStr ;
let c₃ be Element of c₁;
let c₄ be Element of c₂;
redefine func [ as [c₃,c₄] -> Element of [:a₁,a₂:];
coherence

proof end;

end;

definition

let c₁, c₂ be non empty RelStr ;
let c₃ be Element of [:c₁,c₂:];
redefine func `1 as c₃ `1 -> Element of a₁;
coherence

proof end;

redefine func `2 as c₃ `2 -> Element of a₂;
coherence

proof end;

end;

theorem Th11: :: YELLOW_3:11

for b₁, b₂ being non empty RelStr
for b₃, b₄ being Element of b₁
for b₅, b₆ being Element of b₂ holds
( ( b₃ <= b₄ & b₅ <= b₆ ) iff [b₃,b₅] <= [b₄,b₆] )

proof end;

theorem Th12: :: YELLOW_3:12

for b₁, b₂ being non empty RelStr
for b₃, b₄ being Element of [:b₁,b₂:] holds
( b₃ <= b₄ iff ( b₃ `1 <= b₄ `1 & b₃ `2 <= b₄ `2 ) )

proof end;

theorem Th13: :: YELLOW_3:13

for b₁, b₂ being RelStr
for b₃ being non empty RelStr
for b₄, b₅ being Function of [:b₁,b₂:],b₃ st ( for b₆ being Element of b₁
for b₇ being Element of b₂ holds b₄ . [b₆,b₇] = b₅ . [b₆,b₇] ) holds
b₄ = b₅

proof end;

registration

let c₁, c₂ be non empty RelStr ;
cluster [:a₁,a₂:] -> non empty strict ;
coherence

proof end;

end;

registration

let c₁, c₂ be reflexive RelStr ;
cluster [:a₁,a₂:] -> strict reflexive ;
coherence

proof end;

end;

registration

let c₁, c₂ be antisymmetric RelStr ;
cluster [:a₁,a₂:] -> strict antisymmetric ;
coherence

proof end;

end;

registration

let c₁, c₂ be transitive RelStr ;
cluster [:a₁,a₂:] -> strict transitive ;
coherence

proof end;

end;

registration

let c₁, c₂ be with_suprema RelStr ;
cluster [:a₁,a₂:] -> non empty strict with_suprema ;
coherence

proof end;

end;

registration

let c₁, c₂ be with_infima RelStr ;
cluster [:a₁,a₂:] -> non empty strict with_infima ;
coherence

proof end;

end;

theorem Th14: :: YELLOW_3:14

for b₁, b₂ being RelStr st not [:b₁,b₂:] is empty holds
( not b₁ is empty & not b₂ is empty )

proof end;

theorem Th15: :: YELLOW_3:15

for b₁, b₂ being non empty RelStr st [:b₁,b₂:] is reflexive holds
( b₁ is reflexive & b₂ is reflexive )

proof end;

theorem Th16: :: YELLOW_3:16

for b₁, b₂ being non empty reflexive RelStr st [:b₁,b₂:] is antisymmetric holds
( b₁ is antisymmetric & b₂ is antisymmetric )

proof end;

theorem Th17: :: YELLOW_3:17

for b₁, b₂ being non empty reflexive RelStr st [:b₁,b₂:] is transitive holds
( b₁ is transitive & b₂ is transitive )

proof end;

theorem Th18: :: YELLOW_3:18

for b₁, b₂ being non empty reflexive RelStr st [:b₁,b₂:] is with_suprema holds
( b₁ is with_suprema & b₂ is with_suprema )

proof end;

theorem Th19: :: YELLOW_3:19

for b₁, b₂ being non empty reflexive RelStr st [:b₁,b₂:] is with_infima holds
( b₁ is with_infima & b₂ is with_infima )

proof end;

definition

let c₁, c₂ be RelStr ;
let c₃ be directed Subset of c₁;
let c₄ be directed Subset of c₂;
redefine func [: as [:c₃,c₄:] -> directed Subset of [:a₁,a₂:];
coherence

proof end;

end;

theorem Th20: :: YELLOW_3:20

for b₁, b₂ being non empty RelStr
for b₃ being non empty Subset of b₁
for b₄ being non empty Subset of b₂ st [:b₃,b₄:] is directed holds
( b₃ is directed & b₄ is directed )

proof end;

theorem Th21: :: YELLOW_3:21

for b₁, b₂ being non empty RelStr
for b₃ being non empty Subset of [:b₁,b₂:] holds
( not proj1 b₃ is empty & not proj2 b₃ is empty )

proof end;

theorem Th22: :: YELLOW_3:22

for b₁, b₂ being non empty reflexive RelStr
for b₃ being non empty directed Subset of [:b₁,b₂:] holds
( proj1 b₃ is directed & proj2 b₃ is directed )

proof end;

definition

let c₁, c₂ be RelStr ;
let c₃ be filtered Subset of c₁;
let c₄ be filtered Subset of c₂;
redefine func [: as [:c₃,c₄:] -> filtered Subset of [:a₁,a₂:];
coherence

proof end;

end;

theorem Th23: :: YELLOW_3:23

for b₁, b₂ being non empty RelStr
for b₃ being non empty Subset of b₁
for b₄ being non empty Subset of b₂ st [:b₃,b₄:] is filtered holds
( b₃ is filtered & b₄ is filtered )

proof end;

theorem Th24: :: YELLOW_3:24

for b₁, b₂ being non empty reflexive RelStr
for b₃ being non empty filtered Subset of [:b₁,b₂:] holds
( proj1 b₃ is filtered & proj2 b₃ is filtered )

proof end;

definition

let c₁, c₂ be RelStr ;
let c₃ be upper Subset of c₁;
let c₄ be upper Subset of c₂;
redefine func [: as [:c₃,c₄:] -> upper Subset of [:a₁,a₂:];
coherence

proof end;

end;

theorem Th25: :: YELLOW_3:25

for b₁, b₂ being non empty reflexive RelStr
for b₃ being non empty Subset of b₁
for b₄ being non empty Subset of b₂ st [:b₃,b₄:] is upper holds
( b₃ is upper & b₄ is upper )

proof end;

theorem Th26: :: YELLOW_3:26

for b₁, b₂ being non empty reflexive RelStr
for b₃ being non empty upper Subset of [:b₁,b₂:] holds
( proj1 b₃ is upper & proj2 b₃ is upper )

proof end;

definition

let c₁, c₂ be RelStr ;
let c₃ be lower Subset of c₁;
let c₄ be lower Subset of c₂;
redefine func [: as [:c₃,c₄:] -> lower Subset of [:a₁,a₂:];
coherence

proof end;

end;

theorem Th27: :: YELLOW_3:27

for b₁, b₂ being non empty reflexive RelStr
for b₃ being non empty Subset of b₁
for b₄ being non empty Subset of b₂ st [:b₃,b₄:] is lower holds
( b₃ is lower & b₄ is lower )

proof end;

theorem Th28: :: YELLOW_3:28

for b₁, b₂ being non empty reflexive RelStr
for b₃ being non empty lower Subset of [:b₁,b₂:] holds
( proj1 b₃ is lower & proj2 b₃ is lower )

proof end;

definition

let c₁ be RelStr ;
attr a₁ is void means :Def3: :: YELLOW_3:def 3
the InternalRel of a₁ is empty;

end;

:: deftheorem Def3 defines void YELLOW_3:def 3 :

registration

cluster empty -> void RelStr ;
coherence

proof end;

end;

registration

cluster non empty strict non void RelStr ;
existence

proof end;

end;

registration

cluster non void -> non empty RelStr ;
coherence

proof end;

end;

registration

cluster non empty reflexive -> non empty non void RelStr ;
coherence

proof end;

end;

registration

let c₁ be non void RelStr ;
cluster the InternalRel of a₁ -> non empty ;
coherence by Def3;

end;

theorem Th29: :: YELLOW_3:29

for b₁, b₂ being non empty RelStr
for b₃ being non empty Subset of b₁
for b₄ being non empty Subset of b₂
for b₅ being Element of b₁
for b₆ being Element of b₂ st [b₅,b₆] is_>=_than [:b₃,b₄:] holds
( b₅ is_>=_than b₃ & b₆ is_>=_than b₄ )

proof end;

theorem Th30: :: YELLOW_3:30

for b₁, b₂ being non empty RelStr
for b₃ being Subset of b₁
for b₄ being Subset of b₂
for b₅ being Element of b₁
for b₆ being Element of b₂ st b₅ is_>=_than b₃ & b₆ is_>=_than b₄ holds
[b₅,b₆] is_>=_than [:b₃,b₄:]

proof end;

theorem Th31: :: YELLOW_3:31

for b₁, b₂ being non empty RelStr
for b₃ being Subset of [:b₁,b₂:]
for b₄ being Element of b₁
for b₅ being Element of b₂ holds
( [b₄,b₅] is_>=_than b₃ iff ( b₄ is_>=_than proj1 b₃ & b₅ is_>=_than proj2 b₃ ) )

proof end;

theorem Th32: :: YELLOW_3:32

for b₁, b₂ being non empty RelStr
for b₃ being non empty Subset of b₁
for b₄ being non empty Subset of b₂
for b₅ being Element of b₁
for b₆ being Element of b₂ st [b₅,b₆] is_<=_than [:b₃,b₄:] holds
( b₅ is_<=_than b₃ & b₆ is_<=_than b₄ )

proof end;

theorem Th33: :: YELLOW_3:33

for b₁, b₂ being non empty RelStr
for b₃ being Subset of b₁
for b₄ being Subset of b₂
for b₅ being Element of b₁
for b₆ being Element of b₂ st b₅ is_<=_than b₃ & b₆ is_<=_than b₄ holds
[b₅,b₆] is_<=_than [:b₃,b₄:]

proof end;

theorem Th34: :: YELLOW_3:34

for b₁, b₂ being non empty RelStr
for b₃ being Subset of [:b₁,b₂:]
for b₄ being Element of b₁
for b₅ being Element of b₂ holds
( [b₄,b₅] is_<=_than b₃ iff ( b₄ is_<=_than proj1 b₃ & b₅ is_<=_than proj2 b₃ ) )

proof end;

theorem Th35: :: YELLOW_3:35

for b₁, b₂ being non empty antisymmetric RelStr
for b₃ being Subset of b₁
for b₄ being Subset of b₂
for b₅ being Element of b₁
for b₆ being Element of b₂ st ex_sup_of b₃,b₁ & ex_sup_of b₄,b₂ & ( for b₇ being Element of [:b₁,b₂:] st b₇ is_>=_than [:b₃,b₄:] holds
[b₅,b₆] <= b₇ ) holds
( ( for b₇ being Element of b₁ st b₇ is_>=_than b₃ holds
b₅ <= b₇ ) & ( for b₇ being Element of b₂ st b₇ is_>=_than b₄ holds
b₆ <= b₇ ) )

proof end;

theorem Th36: :: YELLOW_3:36

for b₁, b₂ being non empty antisymmetric RelStr
for b₃ being Subset of b₁
for b₄ being Subset of b₂
for b₅ being Element of b₁
for b₆ being Element of b₂ st ex_inf_of b₃,b₁ & ex_inf_of b₄,b₂ & ( for b₇ being Element of [:b₁,b₂:] st b₇ is_<=_than [:b₃,b₄:] holds
[b₅,b₆] >= b₇ ) holds
( ( for b₇ being Element of b₁ st b₇ is_<=_than b₃ holds
b₅ >= b₇ ) & ( for b₇ being Element of b₂ st b₇ is_<=_than b₄ holds
b₆ >= b₇ ) )

proof end;

theorem Th37: :: YELLOW_3:37

for b₁, b₂ being non empty antisymmetric RelStr
for b₃ being non empty Subset of b₁
for b₄ being non empty Subset of b₂
for b₅ being Element of b₁
for b₆ being Element of b₂ st ( for b₇ being Element of b₁ st b₇ is_>=_than b₃ holds
b₅ <= b₇ ) & ( for b₇ being Element of b₂ st b₇ is_>=_than b₄ holds
b₆ <= b₇ ) holds
for b₇ being Element of [:b₁,b₂:] st b₇ is_>=_than [:b₃,b₄:] holds
[b₅,b₆] <= b₇

proof end;

theorem Th38: :: YELLOW_3:38

for b₁, b₂ being non empty antisymmetric RelStr
for b₃ being non empty Subset of b₁
for b₄ being non empty Subset of b₂
for b₅ being Element of b₁
for b₆ being Element of b₂ st ( for b₇ being Element of b₁ st b₇ is_>=_than b₃ holds
b₅ >= b₇ ) & ( for b₇ being Element of b₂ st b₇ is_>=_than b₄ holds
b₆ >= b₇ ) holds
for b₇ being Element of [:b₁,b₂:] st b₇ is_>=_than [:b₃,b₄:] holds
[b₅,b₆] >= b₇

proof end;

theorem Th39: :: YELLOW_3:39

for b₁, b₂ being non empty antisymmetric RelStr
for b₃ being non empty Subset of b₁
for b₄ being non empty Subset of b₂ holds
( ( ex_sup_of b₃,b₁ & ex_sup_of b₄,b₂ ) iff ex_sup_of [:b₃,b₄:],[:b₁,b₂:] )

proof end;

theorem Th40: :: YELLOW_3:40

for b₁, b₂ being non empty antisymmetric RelStr
for b₃ being non empty Subset of b₁
for b₄ being non empty Subset of b₂ holds
( ( ex_inf_of b₃,b₁ & ex_inf_of b₄,b₂ ) iff ex_inf_of [:b₃,b₄:],[:b₁,b₂:] )

proof end;

theorem Th41: :: YELLOW_3:41

for b₁, b₂ being non empty antisymmetric RelStr
for b₃ being Subset of [:b₁,b₂:] holds
( ( ex_sup_of proj1 b₃,b₁ & ex_sup_of proj2 b₃,b₂ ) iff ex_sup_of b₃,[:b₁,b₂:] )

proof end;

theorem Th42: :: YELLOW_3:42

for b₁, b₂ being non empty antisymmetric RelStr
for b₃ being Subset of [:b₁,b₂:] holds
( ( ex_inf_of proj1 b₃,b₁ & ex_inf_of proj2 b₃,b₂ ) iff ex_inf_of b₃,[:b₁,b₂:] )

proof end;

theorem Th43: :: YELLOW_3:43

for b₁, b₂ being non empty antisymmetric RelStr
for b₃ being non empty Subset of b₁
for b₄ being non empty Subset of b₂ st ex_sup_of b₃,b₁ & ex_sup_of b₄,b₂ holds
sup [:b₃,b₄:] = [(sup b₃),(sup b₄)]

proof end;

theorem Th44: :: YELLOW_3:44

for b₁, b₂ being non empty antisymmetric RelStr
for b₃ being non empty Subset of b₁
for b₄ being non empty Subset of b₂ st ex_inf_of b₃,b₁ & ex_inf_of b₄,b₂ holds
inf [:b₃,b₄:] = [(inf b₃),(inf b₄)]

proof end;

registration

let c₁, c₂ be non empty antisymmetric complete RelStr ;
cluster [:a₁,a₂:] -> non empty strict antisymmetric with_suprema with_infima complete ;
coherence

proof end;

end;

theorem Th45: :: YELLOW_3:45

for b₁, b₂ being non empty antisymmetric lower-bounded RelStr st [:b₁,b₂:] is complete holds
( b₁ is complete & b₂ is complete )

proof end;

theorem Th46: :: YELLOW_3:46

for b₁, b₂ being non empty antisymmetric RelStr
for b₃ being non empty Subset of [:b₁,b₂:] st ( [:b₁,b₂:] is complete or ex_sup_of b₃,[:b₁,b₂:] ) holds
sup b₃ = [(sup (proj1 b₃)),(sup (proj2 b₃))]

proof end;

theorem Th47: :: YELLOW_3:47

for b₁, b₂ being non empty antisymmetric RelStr
for b₃ being non empty Subset of [:b₁,b₂:] st ( [:b₁,b₂:] is complete or ex_inf_of b₃,[:b₁,b₂:] ) holds
inf b₃ = [(inf (proj1 b₃)),(inf (proj2 b₃))]

proof end;

theorem Th48: :: YELLOW_3:48

for b₁, b₂ being non empty reflexive RelStr
for b₃ being non empty directed Subset of [:b₁,b₂:] holds [:(proj1 b₃),(proj2 b₃):] c= downarrow b₃

proof end;

theorem Th49: :: YELLOW_3:49

for b₁, b₂ being non empty reflexive RelStr
for b₃ being non empty filtered Subset of [:b₁,b₂:] holds [:(proj1 b₃),(proj2 b₃):] c= uparrow b₃

proof end;

scheme :: YELLOW_3:sch 7
s7{ F₁() -> non empty RelStr , F₂() -> non empty RelStr , F₃() -> non empty RelStr , F₄( set , set ) -> set } :

ex b₁ being Function of [:F₁(),F₂():],F₃() st
for b₂ being Element of F₁()
for b₃ being Element of F₂() holds b₁ . [b₂,b₃] = F₄(b₂,b₃)

provided

E24: for b₁ being Element of F₁()
for b₂ being Element of F₂() holds F₄(b₁,b₂) is Element of F₃()

proof end;