:: FUNCT_6 semantic presentation

begin

theorem :: FUNCT_6:1
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) holds product f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) c= Funcs ((dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( ) ( ) set ) ,(Union f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional ) set ) ;

begin

theorem :: FUNCT_6:2
for x being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st x : ( ( ) ( ) set ) in dom (~ f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) holds
ex y, z being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) = [y : ( ( ) ( ) set ) ,z : ( ( ) ( ) set ) ] : ( ( ) ( V25() ) set ) ;

theorem :: FUNCT_6:3
for X, Y, z being ( ( ) ( ) set ) holds ~ ([:X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) --> z : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like [:b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined {b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) -valued Function-like constant total quasi_total ) Element of bool [:[:b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,{b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) = [:Y : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) --> z : ( ( ) ( ) set ) : ( ( Function-like quasi_total ) ( Relation-like [:b2 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined {b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) -valued Function-like constant total quasi_total ) Element of bool [:[:b2 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,{b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ;

theorem :: FUNCT_6:4
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) holds
( curry f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) = curry' (~ f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) & uncurry f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) = ~ (uncurry' f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ) ;

theorem :: FUNCT_6:5
for X, Y, z being ( ( ) ( ) set ) st [:X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) <> {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) holds
( curry ([:X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) --> z : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like [:b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined {b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) -valued Function-like constant total quasi_total ) Element of bool [:[:b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,{b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) = X : ( ( ) ( ) set ) --> (Y : ( ( ) ( ) set ) --> z : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined {b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) -valued Function-like constant total quasi_total ) Element of bool [:b2 : ( ( ) ( ) set ) ,{b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined {(b2 : ( ( ) ( ) set ) --> b3 : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined {b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) -valued Function-like constant total quasi_total ) Element of bool [:b2 : ( ( ) ( ) set ) ,{b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) } : ( ( ) ( non empty functional V36() ) set ) -valued Function-like constant total quasi_total Function-yielding V35() ) Element of bool [:b1 : ( ( ) ( ) set ) ,{(b2 : ( ( ) ( ) set ) --> b3 : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined {b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) -valued Function-like constant total quasi_total ) Element of bool [:b2 : ( ( ) ( ) set ) ,{b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) } : ( ( ) ( non empty functional V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) & curry' ([:X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) --> z : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like [:b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined {b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) -valued Function-like constant total quasi_total ) Element of bool [:[:b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,{b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) = Y : ( ( ) ( ) set ) --> (X : ( ( ) ( ) set ) --> z : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined {b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) -valued Function-like constant total quasi_total ) Element of bool [:b1 : ( ( ) ( ) set ) ,{b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined {(b1 : ( ( ) ( ) set ) --> b3 : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined {b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) -valued Function-like constant total quasi_total ) Element of bool [:b1 : ( ( ) ( ) set ) ,{b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) } : ( ( ) ( non empty functional V36() ) set ) -valued Function-like constant total quasi_total Function-yielding V35() ) Element of bool [:b2 : ( ( ) ( ) set ) ,{(b1 : ( ( ) ( ) set ) --> b3 : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined {b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) -valued Function-like constant total quasi_total ) Element of bool [:b1 : ( ( ) ( ) set ) ,{b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) } : ( ( ) ( non empty functional V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: FUNCT_6:6
for X, Y, z being ( ( ) ( ) set ) holds
( uncurry (X : ( ( ) ( ) set ) --> (Y : ( ( ) ( ) set ) --> z : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined {b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) -valued Function-like constant total quasi_total ) Element of bool [:b2 : ( ( ) ( ) set ) ,{b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined {(b2 : ( ( ) ( ) set ) --> b3 : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined {b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) -valued Function-like constant total quasi_total ) Element of bool [:b2 : ( ( ) ( ) set ) ,{b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) } : ( ( ) ( non empty functional V36() ) set ) -valued Function-like constant total quasi_total Function-yielding V35() ) Element of bool [:b1 : ( ( ) ( ) set ) ,{(b2 : ( ( ) ( ) set ) --> b3 : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined {b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) -valued Function-like constant total quasi_total ) Element of bool [:b2 : ( ( ) ( ) set ) ,{b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) } : ( ( ) ( non empty functional V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) = [:X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) --> z : ( ( ) ( ) set ) : ( ( Function-like quasi_total ) ( Relation-like [:b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined {b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) -valued Function-like constant total quasi_total ) Element of bool [:[:b1 : ( ( ) ( ) set ) ,b2 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,{b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) & uncurry' (X : ( ( ) ( ) set ) --> (Y : ( ( ) ( ) set ) --> z : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined {b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) -valued Function-like constant total quasi_total ) Element of bool [:b2 : ( ( ) ( ) set ) ,{b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined {(b2 : ( ( ) ( ) set ) --> b3 : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined {b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) -valued Function-like constant total quasi_total ) Element of bool [:b2 : ( ( ) ( ) set ) ,{b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) } : ( ( ) ( non empty functional V36() ) set ) -valued Function-like constant total quasi_total Function-yielding V35() ) Element of bool [:b1 : ( ( ) ( ) set ) ,{(b2 : ( ( ) ( ) set ) --> b3 : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined {b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) -valued Function-like constant total quasi_total ) Element of bool [:b2 : ( ( ) ( ) set ) ,{b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) } : ( ( ) ( non empty functional V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) = [:Y : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) --> z : ( ( ) ( ) set ) : ( ( Function-like quasi_total ) ( Relation-like [:b2 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) -defined {b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) -valued Function-like constant total quasi_total ) Element of bool [:[:b2 : ( ( ) ( ) set ) ,b1 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,{b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: FUNCT_6:7
for x being ( ( ) ( ) set )
for f, g being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st x : ( ( ) ( ) set ) in dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) & g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) = f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
( rng g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) c= rng (uncurry f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) & rng g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) c= rng (uncurry' f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) ) ;

theorem :: FUNCT_6:8
for X being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) holds
( dom (uncurry (X : ( ( ) ( ) set ) --> f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined {b2 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) } : ( ( ) ( non empty functional V36() ) set ) -valued Function-like constant total quasi_total Function-yielding V35() ) Element of bool [:b1 : ( ( ) ( ) set ) ,{b2 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) } : ( ( ) ( non empty functional V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) = [:X : ( ( ) ( ) set ) ,(dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) & rng (uncurry (X : ( ( ) ( ) set ) --> f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined {b2 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) } : ( ( ) ( non empty functional V36() ) set ) -valued Function-like constant total quasi_total Function-yielding V35() ) Element of bool [:b1 : ( ( ) ( ) set ) ,{b2 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) } : ( ( ) ( non empty functional V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) c= rng f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) & dom (uncurry' (X : ( ( ) ( ) set ) --> f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined {b2 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) } : ( ( ) ( non empty functional V36() ) set ) -valued Function-like constant total quasi_total Function-yielding V35() ) Element of bool [:b1 : ( ( ) ( ) set ) ,{b2 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) } : ( ( ) ( non empty functional V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) = [:(dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) & rng (uncurry' (X : ( ( ) ( ) set ) --> f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined {b2 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) } : ( ( ) ( non empty functional V36() ) set ) -valued Function-like constant total quasi_total Function-yielding V35() ) Element of bool [:b1 : ( ( ) ( ) set ) ,{b2 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) } : ( ( ) ( non empty functional V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) c= rng f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) ) ;

theorem :: FUNCT_6:9
for X being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st X : ( ( ) ( ) set ) <> {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) holds
( rng (uncurry (X : ( ( ) ( ) set ) --> f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined {b2 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) } : ( ( ) ( non empty functional V36() ) set ) -valued Function-like constant total quasi_total Function-yielding V35() ) Element of bool [:b1 : ( ( ) ( ) set ) ,{b2 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) } : ( ( ) ( non empty functional V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) = rng f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) & rng (uncurry' (X : ( ( ) ( ) set ) --> f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined {b2 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) } : ( ( ) ( non empty functional V36() ) set ) -valued Function-like constant total quasi_total Function-yielding V35() ) Element of bool [:b1 : ( ( ) ( ) set ) ,{b2 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) } : ( ( ) ( non empty functional V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) = rng f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) ) ;

theorem :: FUNCT_6:10
for X, Y, Z being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st [:X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) <> {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) & f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) in Funcs ([:X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,Z : ( ( ) ( ) set ) ) : ( ( ) ( functional ) set ) holds
( curry f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) in Funcs (X : ( ( ) ( ) set ) ,(Funcs (Y : ( ( ) ( ) set ) ,Z : ( ( ) ( ) set ) )) : ( ( ) ( functional ) set ) ) : ( ( ) ( functional ) set ) & curry' f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) in Funcs (Y : ( ( ) ( ) set ) ,(Funcs (X : ( ( ) ( ) set ) ,Z : ( ( ) ( ) set ) )) : ( ( ) ( functional ) set ) ) : ( ( ) ( functional ) set ) ) ;

theorem :: FUNCT_6:11
for X, Y, Z being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) in Funcs (X : ( ( ) ( ) set ) ,(Funcs (Y : ( ( ) ( ) set ) ,Z : ( ( ) ( ) set ) )) : ( ( ) ( functional ) set ) ) : ( ( ) ( functional ) set ) holds
( uncurry f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) in Funcs ([:X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,Z : ( ( ) ( ) set ) ) : ( ( ) ( functional ) set ) & uncurry' f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) in Funcs ([:Y : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,Z : ( ( ) ( ) set ) ) : ( ( ) ( functional ) set ) ) ;

theorem :: FUNCT_6:12
for X, Y, Z, V1, V2 being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st ( curry f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) in Funcs (X : ( ( ) ( ) set ) ,(Funcs (Y : ( ( ) ( ) set ) ,Z : ( ( ) ( ) set ) )) : ( ( ) ( functional ) set ) ) : ( ( ) ( functional ) set ) or curry' f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) in Funcs (Y : ( ( ) ( ) set ) ,(Funcs (X : ( ( ) ( ) set ) ,Z : ( ( ) ( ) set ) )) : ( ( ) ( functional ) set ) ) : ( ( ) ( functional ) set ) ) & dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) c= [:V1 : ( ( ) ( ) set ) ,V2 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) holds
f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) in Funcs ([:X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,Z : ( ( ) ( ) set ) ) : ( ( ) ( functional ) set ) ;

theorem :: FUNCT_6:13
for X, Y, Z, V1, V2 being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st ( uncurry f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) in Funcs ([:X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,Z : ( ( ) ( ) set ) ) : ( ( ) ( functional ) set ) or uncurry' f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) in Funcs ([:Y : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,Z : ( ( ) ( ) set ) ) : ( ( ) ( functional ) set ) ) & rng f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) c= PFuncs (V1 : ( ( ) ( ) set ) ,V2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) & dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) = X : ( ( ) ( ) set ) holds
f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) in Funcs (X : ( ( ) ( ) set ) ,(Funcs (Y : ( ( ) ( ) set ) ,Z : ( ( ) ( ) set ) )) : ( ( ) ( functional ) set ) ) : ( ( ) ( functional ) set ) ;

theorem :: FUNCT_6:14
for X, Y, Z being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) in PFuncs ([:X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) holds
( curry f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) in PFuncs (X : ( ( ) ( ) set ) ,(PFuncs (Y : ( ( ) ( ) set ) ,Z : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) & curry' f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) in PFuncs (Y : ( ( ) ( ) set ) ,(PFuncs (X : ( ( ) ( ) set ) ,Z : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: FUNCT_6:15
for X, Y, Z being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) in PFuncs (X : ( ( ) ( ) set ) ,(PFuncs (Y : ( ( ) ( ) set ) ,Z : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) holds
( uncurry f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) in PFuncs ([:X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) & uncurry' f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) in PFuncs ([:Y : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ;

theorem :: FUNCT_6:16
for X, Y, Z, V1, V2 being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st ( curry f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) in PFuncs (X : ( ( ) ( ) set ) ,(PFuncs (Y : ( ( ) ( ) set ) ,Z : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) or curry' f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) in PFuncs (Y : ( ( ) ( ) set ) ,(PFuncs (X : ( ( ) ( ) set ) ,Z : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) c= [:V1 : ( ( ) ( ) set ) ,V2 : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) holds
f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) in PFuncs ([:X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ;

theorem :: FUNCT_6:17
for X, Y, Z, V1, V2 being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st ( uncurry f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) in PFuncs ([:X : ( ( ) ( ) set ) ,Y : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) or uncurry' f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) in PFuncs ([:Y : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ,Z : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) & rng f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) c= PFuncs (V1 : ( ( ) ( ) set ) ,V2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) & dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) holds
f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) in PFuncs (X : ( ( ) ( ) set ) ,(PFuncs (Y : ( ( ) ( ) set ) ,Z : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ;

begin

definition
let X be ( ( ) ( ) set ) ;
func SubFuncs X -> ( ( ) ( ) set ) means :: FUNCT_6:def 1
 for x being ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in it : ( ( ) ( ) set ) iff ( x : ( ( ) ( ) set ) in X : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) & x : ( ( ) ( ) set ) is ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) );
end;

theorem :: FUNCT_6:18
for X being ( ( ) ( ) set ) holds SubFuncs X : ( ( ) ( ) set ) : ( ( ) ( ) set ) c= X : ( ( ) ( ) set ) ;

theorem :: FUNCT_6:19
for x being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) holds
( x : ( ( ) ( ) set ) in f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) " (SubFuncs (rng f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) iff ( x : ( ( ) ( ) set ) in dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) & f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) is ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) ) ;

theorem :: FUNCT_6:20
for f, g, h being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) holds
( SubFuncs {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) : ( ( ) ( ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) & SubFuncs {f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) } : ( ( ) ( non empty functional V36() ) set ) : ( ( ) ( ) set ) = {f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) } : ( ( ) ( non empty functional V36() ) set ) & SubFuncs {f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ,g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) } : ( ( ) ( non empty functional V36() ) set ) : ( ( ) ( ) set ) = {f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ,g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) } : ( ( ) ( non empty functional V36() ) set ) & SubFuncs {f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ,g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ,h : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) } : ( ( ) ( V36() ) set ) : ( ( ) ( ) set ) = {f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ,g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ,h : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) } : ( ( ) ( V36() ) set ) ) ;

theorem :: FUNCT_6:21
for Y, X being ( ( ) ( ) set ) st Y : ( ( ) ( ) set ) c= SubFuncs X : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
SubFuncs Y : ( ( ) ( ) set ) : ( ( ) ( ) set ) = Y : ( ( ) ( ) set ) ;

definition
let f be ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ;
func doms f -> ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) means :: FUNCT_6:def 2
( dom it : ( ( ) ( ) set ) : ( ( ) ( ) set ) = f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) " (SubFuncs (rng f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) & ( for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) " (SubFuncs (rng f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
it : ( ( ) ( ) set ) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) = proj1 (f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) . x : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) );
func rngs f -> ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) means :: FUNCT_6:def 3
( dom it : ( ( ) ( ) set ) : ( ( ) ( ) set ) = f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) " (SubFuncs (rng f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) & ( for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) " (SubFuncs (rng f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
it : ( ( ) ( ) set ) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) = proj2 (f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) . x : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) );
func meet f -> ( ( ) ( ) set ) equals :: FUNCT_6:def 4
 meet (rng f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;
end;

theorem :: FUNCT_6:22
for x being ( ( ) ( ) set )
for f, g being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st x : ( ( ) ( ) set ) in dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) & g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) = f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in dom (doms f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) & (doms f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) = dom g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) & x : ( ( ) ( ) set ) in dom (rngs f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) & (rngs f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) = rng g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) ) ;

theorem :: FUNCT_6:23
( doms {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) & rngs {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) ) ;

theorem :: FUNCT_6:24
for X being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) holds
( doms (X : ( ( ) ( ) set ) --> f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined {b2 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) } : ( ( ) ( non empty functional V36() ) set ) -valued Function-like constant total quasi_total Function-yielding V35() ) Element of bool [:b1 : ( ( ) ( ) set ) ,{b2 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) } : ( ( ) ( non empty functional V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) = X : ( ( ) ( ) set ) --> (dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( ) ( ) set ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined {(dom b2 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) -valued Function-like constant total quasi_total ) Element of bool [:b1 : ( ( ) ( ) set ) ,{(dom b2 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) & rngs (X : ( ( ) ( ) set ) --> f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined {b2 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) } : ( ( ) ( non empty functional V36() ) set ) -valued Function-like constant total quasi_total Function-yielding V35() ) Element of bool [:b1 : ( ( ) ( ) set ) ,{b2 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) } : ( ( ) ( non empty functional V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) = X : ( ( ) ( ) set ) --> (rng f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( ) ( ) set ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined {(rng b2 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) -valued Function-like constant total quasi_total ) Element of bool [:b1 : ( ( ) ( ) set ) ,{(rng b2 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ) ;

theorem :: FUNCT_6:25
for x being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) <> {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) holds
( x : ( ( ) ( ) set ) in meet f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) iff for y being ( ( ) ( ) set ) st y : ( ( ) ( ) set ) in dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) holds
x : ( ( ) ( ) set ) in f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . y : ( ( ) ( ) set ) : ( ( ) ( ) set ) ) ;

theorem :: FUNCT_6:26
for Y being ( ( ) ( ) set ) holds
( Union ({} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) --> Y : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( empty Relation-like non-empty empty-yielding {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) -defined {b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) -valued Function-like one-to-one constant functional total V18() V19() V20() V22() V23() V24() quasi_total Function-yielding V35() V36() V37() V40() ) Element of bool [:{} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) ,{b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) :] : ( ( ) ( Relation-like V36() ) set ) : ( ( ) ( V36() V40() ) set ) ) : ( ( ) ( ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) & meet ({} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) --> Y : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( empty Relation-like non-empty empty-yielding {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) -defined {b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) -valued Function-like one-to-one constant functional total V18() V19() V20() V22() V23() V24() quasi_total Function-yielding V35() V36() V37() V40() ) Element of bool [:{} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) ,{b1 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) :] : ( ( ) ( Relation-like V36() ) set ) : ( ( ) ( V36() V40() ) set ) ) : ( ( ) ( ) set ) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) ) ;

theorem :: FUNCT_6:27
for X, Y being ( ( ) ( ) set ) st X : ( ( ) ( ) set ) <> {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) holds
( Union (X : ( ( ) ( ) set ) --> Y : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined {b2 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) -valued Function-like constant total quasi_total Function-yielding V35() ) Element of bool [:b1 : ( ( ) ( ) set ) ,{b2 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) = Y : ( ( ) ( ) set ) & meet (X : ( ( ) ( ) set ) --> Y : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined {b2 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) -valued Function-like constant total quasi_total Function-yielding V35() ) Element of bool [:b1 : ( ( ) ( ) set ) ,{b2 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) = Y : ( ( ) ( ) set ) ) ;

definition
let f be ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ;
let x, y be ( ( ) ( ) set ) ;
func f .. (x,y) -> ( ( ) ( ) set ) equals :: FUNCT_6:def 5
(uncurry f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) . (x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ;
end;

theorem :: FUNCT_6:28
for x, X, y being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st x : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) & y : ( ( ) ( ) set ) in dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) holds
(X : ( ( ) ( ) set ) --> f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Function-like quasi_total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined {b4 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) } : ( ( ) ( non empty functional V36() ) set ) -valued Function-like constant total quasi_total Function-yielding V35() ) Element of bool [:b2 : ( ( ) ( ) set ) ,{b4 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) } : ( ( ) ( non empty functional V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) .. (x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) = f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . y : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

begin

definition
let f be ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ;
func <:f:> -> ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) equals :: FUNCT_6:def 6
 curry ((uncurry' f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) | [:(meet (doms f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( ) ( ) set ) ,(dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ) : ( ( Relation-like ) ( Relation-like Function-like ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ;
end;

theorem :: FUNCT_6:29
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) holds
( dom <:f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) :> : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) = meet (doms f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) & rng <:f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) :> : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) c= product (rngs f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) ) ;

theorem :: FUNCT_6:30
for x being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st x : ( ( ) ( ) set ) in dom <:f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) :> : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) holds
<:f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) :> : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) is ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ;

theorem :: FUNCT_6:31
for x being ( ( ) ( ) set )
for f, g being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st x : ( ( ) ( ) set ) in dom <:f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) :> : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) & g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) = <:f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) :> : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
( dom g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) = f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) " (SubFuncs (rng f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) & ( for y being ( ( ) ( ) set ) st y : ( ( ) ( ) set ) in dom g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) holds
( [y : ( ( ) ( ) set ) ,x : ( ( ) ( ) set ) ] : ( ( ) ( V25() ) set ) in dom (uncurry f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) & g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . y : ( ( ) ( ) set ) : ( ( ) ( ) set ) = (uncurry f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) . (y : ( ( ) ( ) set ) ,x : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: FUNCT_6:32
for x being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st x : ( ( ) ( ) set ) in dom <:f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) :> : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) holds
for g being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) in rng f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) holds
x : ( ( ) ( ) set ) in dom g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) ;

theorem :: FUNCT_6:33
for x being ( ( ) ( ) set )
for g, f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) in rng f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) & ( for g being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) in rng f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) holds
x : ( ( ) ( ) set ) in dom g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) ) holds
x : ( ( ) ( ) set ) in dom <:f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) :> : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) ;

theorem :: FUNCT_6:34
for x, y being ( ( ) ( ) set )
for f, g, h being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st x : ( ( ) ( ) set ) in dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) & g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) = f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) & y : ( ( ) ( ) set ) in dom <:f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) :> : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) & h : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) = <:f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) :> : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . y : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . y : ( ( ) ( ) set ) : ( ( ) ( ) set ) = h : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: FUNCT_6:35
for x, y being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st x : ( ( ) ( ) set ) in dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) & f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) is ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) & y : ( ( ) ( ) set ) in dom <:f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) :> : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) holds
f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) .. (x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) = <:f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) :> : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) .. (y : ( ( ) ( ) set ) ,x : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ;

definition
let f be ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ;
func Frege f -> ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) means :: FUNCT_6:def 7
( dom it : ( ( ) ( ) set ) : ( ( ) ( ) set ) = product (doms f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) & ( for g being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) in product (doms f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) holds
ex h being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st
( it : ( ( ) ( ) set ) . g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) = h : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) & dom h : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) = f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) " (SubFuncs (rng f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) & ( for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in dom h : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) holds
h : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) = (uncurry f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) . (x : ( ( ) ( ) set ) ,(g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) ) ) );
end;

theorem :: FUNCT_6:36
for x being ( ( ) ( ) set )
for g, f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) in product (doms f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) & x : ( ( ) ( ) set ) in dom g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) holds
(Frege f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) .. (g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ,x : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) = f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) .. (x : ( ( ) ( ) set ) ,(g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ;

theorem :: FUNCT_6:37
for x being ( ( ) ( ) set )
for f, g, h, h9 being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st x : ( ( ) ( ) set ) in dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) & g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) = f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) & h : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) in product (doms f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) & h9 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) = (Frege f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . h : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) holds
( h : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) in dom g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) & h9 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) = g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . (h : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) & h9 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) in product (rngs f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) ) ;

theorem :: FUNCT_6:38
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) holds rng (Frege f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) = product (rngs f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) ;

theorem :: FUNCT_6:39
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st not {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) in rng f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) holds
( Frege f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) is one-to-one iff for g being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) in rng f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) holds
g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) is one-to-one ) ;

begin

theorem :: FUNCT_6:40
( <:{} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) :> : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) & Frege {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) .--> {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) : ( ( ) ( Relation-like {{} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) } : ( ( ) ( non empty functional V36() V40() ) set ) -defined Function-like one-to-one Function-yielding V35() V36() ) set ) ) ;

theorem :: FUNCT_6:41
for X being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st X : ( ( ) ( ) set ) <> {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) holds
( dom <:(X : ( ( ) ( ) set ) --> f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined {b2 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) } : ( ( ) ( non empty functional V36() ) set ) -valued Function-like constant total quasi_total Function-yielding V35() ) Element of bool [:b1 : ( ( ) ( ) set ) ,{b2 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) } : ( ( ) ( non empty functional V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) :> : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) = dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) & ( for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) holds
<:(X : ( ( ) ( ) set ) --> f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined {b2 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) } : ( ( ) ( non empty functional V36() ) set ) -valued Function-like constant total quasi_total Function-yielding V35() ) Element of bool [:b1 : ( ( ) ( ) set ) ,{b2 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) } : ( ( ) ( non empty functional V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) :> : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) = X : ( ( ) ( ) set ) --> (f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined {(b2 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . b3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) -valued Function-like constant total quasi_total ) Element of bool [:b1 : ( ( ) ( ) set ) ,{(b2 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . b3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: FUNCT_6:42
for X being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) holds
( dom (Frege (X : ( ( ) ( ) set ) --> f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined {b2 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) } : ( ( ) ( non empty functional V36() ) set ) -valued Function-like constant total quasi_total Function-yielding V35() ) Element of bool [:b1 : ( ( ) ( ) set ) ,{b2 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) } : ( ( ) ( non empty functional V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) = Funcs (X : ( ( ) ( ) set ) ,(dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional ) set ) & rng (Frege (X : ( ( ) ( ) set ) --> f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined {b2 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) } : ( ( ) ( non empty functional V36() ) set ) -valued Function-like constant total quasi_total Function-yielding V35() ) Element of bool [:b1 : ( ( ) ( ) set ) ,{b2 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) } : ( ( ) ( non empty functional V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) = Funcs (X : ( ( ) ( ) set ) ,(rng f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional ) set ) & ( for g being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) in Funcs (X : ( ( ) ( ) set ) ,(dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional ) set ) holds
(Frege (X : ( ( ) ( ) set ) --> f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined {b2 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) } : ( ( ) ( non empty functional V36() ) set ) -valued Function-like constant total quasi_total Function-yielding V35() ) Element of bool [:b1 : ( ( ) ( ) set ) ,{b2 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) } : ( ( ) ( non empty functional V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) = f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) * g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( Relation-like ) ( Relation-like Function-like ) set ) ) ) ;

theorem :: FUNCT_6:43
for X being ( ( ) ( ) set )
for f, g being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) = X : ( ( ) ( ) set ) & dom g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) = X : ( ( ) ( ) set ) & ( for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in X : ( ( ) ( ) set ) holds
f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) ,g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) are_equipotent ) holds
product f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) , product g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) are_equipotent ;

theorem :: FUNCT_6:44
for f, h, g being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) = dom h : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) & dom g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) = rng h : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) & h : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) is one-to-one & ( for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in dom h : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) holds
f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) ,g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . (h : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) are_equipotent ) holds
product f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) , product g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) are_equipotent ;

theorem :: FUNCT_6:45
for X being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function)
for P being ( ( Function-like quasi_total bijective ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued Function-like one-to-one total quasi_total onto bijective ) Permutation of X : ( ( ) ( ) set ) ) st dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) = X : ( ( ) ( ) set ) holds
product f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) , product (f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) * P : ( ( Function-like quasi_total bijective ) ( Relation-like b1 : ( ( ) ( ) set ) -defined b1 : ( ( ) ( ) set ) -valued Function-like one-to-one total quasi_total onto bijective ) Permutation of b1 : ( ( ) ( ) set ) ) ) : ( ( Relation-like ) ( Relation-like b1 : ( ( ) ( ) set ) -defined Function-like ) set ) : ( ( ) ( ) set ) are_equipotent ;

begin

definition
let f be ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ;
let X be ( ( ) ( ) set ) ;
func Funcs (f,X) -> ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) means :: FUNCT_6:def 8
( dom it : ( ( ) ( ) set ) : ( ( ) ( ) set ) = dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) & ( for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( ) ( ) set ) holds
it : ( ( ) ( ) set ) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) = Funcs ((f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) . x : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) ) : ( ( ) ( functional ) set ) ) );
end;

theorem :: FUNCT_6:46
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st not {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) in rng f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) holds
Funcs (f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ,{} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) = (dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( ) ( ) set ) --> {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) : ( ( Function-like quasi_total ) ( Relation-like dom b1 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) -defined {{} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) } : ( ( ) ( non empty functional V36() V40() ) set ) -valued Function-like constant total quasi_total Function-yielding V35() ) Element of bool [:(dom b1 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( ) ( ) set ) ,{{} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) } : ( ( ) ( non empty functional V36() V40() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ;

theorem :: FUNCT_6:47
for X being ( ( ) ( ) set ) holds Funcs ({} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) ,X : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) ;

theorem :: FUNCT_6:48
for X, Y, Z being ( ( ) ( ) set ) holds Funcs ((X : ( ( ) ( ) set ) --> Y : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined {b2 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) -valued Function-like constant total quasi_total Function-yielding V35() ) Element of bool [:b1 : ( ( ) ( ) set ) ,{b2 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ,Z : ( ( ) ( ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) = X : ( ( ) ( ) set ) --> (Funcs (Y : ( ( ) ( ) set ) ,Z : ( ( ) ( ) set ) )) : ( ( ) ( functional ) set ) : ( ( Function-like quasi_total ) ( Relation-like b1 : ( ( ) ( ) set ) -defined {(Funcs (b2 : ( ( ) ( ) set ) ,b3 : ( ( ) ( ) set ) )) : ( ( ) ( functional ) set ) } : ( ( ) ( non empty V36() ) set ) -valued Function-like constant total quasi_total ) Element of bool [:b1 : ( ( ) ( ) set ) ,{(Funcs (b2 : ( ( ) ( ) set ) ,b3 : ( ( ) ( ) set ) )) : ( ( ) ( functional ) set ) } : ( ( ) ( non empty V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ;

theorem :: FUNCT_6:49
for X being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) holds Funcs ((Union (disjoin f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ) : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) ) : ( ( ) ( functional ) set ) , product (Funcs (f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ,X : ( ( ) ( ) set ) )) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) are_equipotent ;

definition
let X be ( ( ) ( ) set ) ;
let f be ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ;
func Funcs (X,f) -> ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) means :: FUNCT_6:def 9
( dom it : ( ( ) ( ) set ) : ( ( ) ( ) set ) = dom f : ( ( ) ( ) set ) : ( ( ) ( ) set ) & ( for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in dom f : ( ( ) ( ) set ) : ( ( ) ( ) set ) holds
it : ( ( ) ( ) set ) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) = Funcs (X : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ,(f : ( ( ) ( ) set ) . x : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional ) set ) ) );
end;

theorem :: FUNCT_6:50
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) holds Funcs ({} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) ,f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) = (dom f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( ) ( ) set ) --> {{} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) } : ( ( ) ( non empty functional V36() V40() ) set ) : ( ( Function-like quasi_total ) ( Relation-like non-empty dom b1 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) -defined {{{} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) } : ( ( ) ( non empty functional V36() V40() ) set ) } : ( ( ) ( non empty V36() V40() ) set ) -valued Function-like constant total quasi_total ) Element of bool [:(dom b1 : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( ) ( ) set ) ,{{{} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) } : ( ( ) ( non empty functional V36() V40() ) set ) } : ( ( ) ( non empty V36() V40() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ;

theorem :: FUNCT_6:51
for X being ( ( ) ( ) set ) holds Funcs (X : ( ( ) ( ) set ) ,{} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) ;

theorem :: FUNCT_6:52
for X, Y, Z being ( ( ) ( ) set ) holds Funcs (X : ( ( ) ( ) set ) ,(Y : ( ( ) ( ) set ) --> Z : ( ( ) ( ) set ) ) : ( ( Function-like quasi_total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined {b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) -valued Function-like constant total quasi_total ) Element of bool [:b2 : ( ( ) ( ) set ) ,{b3 : ( ( ) ( ) set ) } : ( ( ) ( non empty V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) = Y : ( ( ) ( ) set ) --> (Funcs (X : ( ( ) ( ) set ) ,Z : ( ( ) ( ) set ) )) : ( ( ) ( functional ) set ) : ( ( Function-like quasi_total ) ( Relation-like b2 : ( ( ) ( ) set ) -defined {(Funcs (b1 : ( ( ) ( ) set ) ,b3 : ( ( ) ( ) set ) )) : ( ( ) ( functional ) set ) } : ( ( ) ( non empty V36() ) set ) -valued Function-like constant total quasi_total ) Element of bool [:b2 : ( ( ) ( ) set ) ,{(Funcs (b1 : ( ( ) ( ) set ) ,b3 : ( ( ) ( ) set ) )) : ( ( ) ( functional ) set ) } : ( ( ) ( non empty V36() ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) ) ;

theorem :: FUNCT_6:53
for X being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) holds product (Funcs (X : ( ( ) ( ) set ) ,f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) )) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) , Funcs (X : ( ( ) ( ) set ) ,(product f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( ) ( ) set ) ) : ( ( ) ( functional ) set ) are_equipotent ;

begin

definition
let f be ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ;
func commute f -> ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding V35() ) Function) equals :: FUNCT_6:def 10
 curry' (uncurry f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) set ) ;
end;

theorem :: FUNCT_6:54
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function)
for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in dom (commute f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding V35() ) Function) : ( ( ) ( ) set ) holds
(commute f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding V35() ) Function) . x : ( ( ) ( ) set ) : ( ( ) ( Relation-like Function-like ) set ) is ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ;

theorem :: FUNCT_6:55
for A, B, C being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st A : ( ( ) ( ) set ) <> {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) & B : ( ( ) ( ) set ) <> {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) & f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) in Funcs (A : ( ( ) ( ) set ) ,(Funcs (B : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional ) set ) ) : ( ( ) ( functional ) set ) holds
commute f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding V35() ) Function) in Funcs (B : ( ( ) ( ) set ) ,(Funcs (A : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional ) set ) ) : ( ( ) ( functional ) set ) ;

theorem :: FUNCT_6:56
for A, B, C being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st A : ( ( ) ( ) set ) <> {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) & B : ( ( ) ( ) set ) <> {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) & f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) in Funcs (A : ( ( ) ( ) set ) ,(Funcs (B : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional ) set ) ) : ( ( ) ( functional ) set ) holds
for g, h being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function)
for x, y being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in A : ( ( ) ( ) set ) & y : ( ( ) ( ) set ) in B : ( ( ) ( ) set ) & f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) = g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) & (commute f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding V35() ) Function) . y : ( ( ) ( ) set ) : ( ( ) ( Relation-like Function-like ) set ) = h : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) holds
( h : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . x : ( ( ) ( ) set ) : ( ( ) ( ) set ) = g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) . y : ( ( ) ( ) set ) : ( ( ) ( ) set ) & dom h : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) = A : ( ( ) ( ) set ) & dom g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) = B : ( ( ) ( ) set ) & rng h : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) c= C : ( ( ) ( ) set ) & rng g : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) c= C : ( ( ) ( ) set ) ) ;

theorem :: FUNCT_6:57
for A, B, C being ( ( ) ( ) set )
for f being ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) st A : ( ( ) ( ) set ) <> {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) & B : ( ( ) ( ) set ) <> {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) & f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) in Funcs (A : ( ( ) ( ) set ) ,(Funcs (B : ( ( ) ( ) set ) ,C : ( ( ) ( ) set ) )) : ( ( ) ( functional ) set ) ) : ( ( ) ( functional ) set ) holds
commute (commute f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ) : ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding V35() ) Function) : ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding V35() ) Function) = f : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ;

theorem :: FUNCT_6:58
commute {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) : ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding V35() ) Function) = {} : ( ( ) ( empty Relation-like non-empty empty-yielding Function-like one-to-one constant functional V18() V19() V20() V22() V23() V24() Function-yielding V35() V36() V37() V40() ) set ) ;

theorem :: FUNCT_6:59
for f being ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding V35() ) Function) holds dom (doms f : ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding V35() ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) = dom f : ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding V35() ) Function) : ( ( ) ( ) set ) ;

theorem :: FUNCT_6:60
for f being ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding V35() ) Function) holds dom (rngs f : ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding V35() ) Function) ) : ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) : ( ( ) ( ) set ) = dom f : ( ( Relation-like Function-like Function-yielding ) ( Relation-like Function-like Function-yielding V35() ) Function) : ( ( ) ( ) set ) ;