:: by Grzegorz Bancerek and Adam Naumowicz

::

:: Received November 26, 1999

:: Copyright (c) 1999-2017 Association of Mizar Users

definition

let F be Function;

end;
attr F is uncurrying means :Def1: :: WAYBEL27:def 1

( ( for x being set st x in dom F holds

x is Function-yielding Function ) & ( for f being Function st f in dom F holds

F . f = uncurry f ) );

( ( for x being set st x in dom F holds

x is Function-yielding Function ) & ( for f being Function st f in dom F holds

F . f = uncurry f ) );

:: deftheorem Def1 defines uncurrying WAYBEL27:def 1 :

for F being Function holds

( F is uncurrying iff ( ( for x being set st x in dom F holds

x is Function-yielding Function ) & ( for f being Function st f in dom F holds

F . f = uncurry f ) ) );

for F being Function holds

( F is uncurrying iff ( ( for x being set st x in dom F holds

x is Function-yielding Function ) & ( for f being Function st f in dom F holds

F . f = uncurry f ) ) );

:: deftheorem Def2 defines currying WAYBEL27:def 2 :

for F being Function holds

( F is currying iff ( ( for x being set st x in dom F holds

( x is Function & proj1 x is Relation ) ) & ( for f being Function st f in dom F holds

F . f = curry f ) ) );

for F being Function holds

( F is currying iff ( ( for x being set st x in dom F holds

( x is Function & proj1 x is Relation ) ) & ( for f being Function st f in dom F holds

F . f = curry f ) ) );

:: deftheorem Def3 defines commuting WAYBEL27:def 3 :

for F being Function holds

( F is commuting iff ( ( for x being set st x in dom F holds

x is Function-yielding Function ) & ( for f being Function st f in dom F holds

F . f = commute f ) ) );

for F being Function holds

( F is commuting iff ( ( for x being set st x in dom F holds

x is Function-yielding Function ) & ( for f being Function st f in dom F holds

F . f = commute f ) ) );

registration

coherence

for b_{1} being Function st b_{1} is empty holds

( b_{1} is uncurrying & b_{1} is currying & b_{1} is commuting )
;

end;
for b

( b

registration

existence

ex b_{1} being Function st

( b_{1} is uncurrying & b_{1} is currying & b_{1} is commuting )

end;
ex b

( b

proof end;

registration
end;

theorem Th1: :: WAYBEL27:1

for X, Y, Z, D being set st D c= Funcs (X,(Funcs (Y,Z))) holds

ex F being ManySortedSet of D st

( F is uncurrying & rng F c= Funcs ([:X,Y:],Z) )

ex F being ManySortedSet of D st

( F is uncurrying & rng F c= Funcs ([:X,Y:],Z) )

proof end;

theorem Th2: :: WAYBEL27:2

for X, Y, Z, D being set st D c= Funcs ([:X,Y:],Z) holds

ex F being ManySortedSet of D st

( F is currying & ( ( Y = {} implies X = {} ) implies rng F c= Funcs (X,(Funcs (Y,Z))) ) )

ex F being ManySortedSet of D st

( F is currying & ( ( Y = {} implies X = {} ) implies rng F c= Funcs (X,(Funcs (Y,Z))) ) )

proof end;

registration

let X, Y, Z be set ;

ex b_{1} being ManySortedSet of Funcs (X,(Funcs (Y,Z))) st b_{1} is uncurrying

ex b_{1} being ManySortedSet of Funcs ([:X,Y:],Z) st b_{1} is currying

end;
cluster Relation-like Funcs (X,(Funcs (Y,Z))) -defined Function-like V27( Funcs (X,(Funcs (Y,Z)))) uncurrying for set ;

existence ex b

proof end;

cluster Relation-like Funcs ([:X,Y:],Z) -defined Function-like V27( Funcs ([:X,Y:],Z)) currying for set ;

existence ex b

proof end;

theorem Th3: :: WAYBEL27:3

for A, B being non empty set

for C being set

for f, g being commuting Function st dom f c= Funcs (A,(Funcs (B,C))) & rng f c= dom g holds

g * f = id (dom f)

for C being set

for f, g being commuting Function st dom f c= Funcs (A,(Funcs (B,C))) & rng f c= dom g holds

g * f = id (dom f)

proof end;

theorem Th4: :: WAYBEL27:4

for B being non empty set

for A, C being set

for f being uncurrying Function

for g being currying Function st dom f c= Funcs (A,(Funcs (B,C))) & rng f c= dom g holds

g * f = id (dom f)

for A, C being set

for f being uncurrying Function

for g being currying Function st dom f c= Funcs (A,(Funcs (B,C))) & rng f c= dom g holds

g * f = id (dom f)

proof end;

theorem Th5: :: WAYBEL27:5

for A, B, C being set

for f being currying Function

for g being uncurrying Function st dom f c= Funcs ([:A,B:],C) & rng f c= dom g holds

g * f = id (dom f)

for f being currying Function

for g being uncurrying Function st dom f c= Funcs ([:A,B:],C) & rng f c= dom g holds

g * f = id (dom f)

proof end;

theorem Th6: :: WAYBEL27:6

for f being Function-yielding Function

for i, A being set st i in dom (commute f) holds

((commute f) . i) .: A c= pi ((f .: A),i)

for i, A being set st i in dom (commute f) holds

((commute f) . i) .: A c= pi ((f .: A),i)

proof end;

theorem Th7: :: WAYBEL27:7

for f being Function-yielding Function

for i, A being set st ( for g being Function st g in f .: A holds

i in dom g ) holds

pi ((f .: A),i) c= ((commute f) . i) .: A

for i, A being set st ( for g being Function st g in f .: A holds

i in dom g ) holds

pi ((f .: A),i) c= ((commute f) . i) .: A

proof end;

theorem Th8: :: WAYBEL27:8

for X, Y being set

for f being Function st rng f c= Funcs (X,Y) holds

for i, A being set st i in X holds

((commute f) . i) .: A = pi ((f .: A),i)

for f being Function st rng f c= Funcs (X,Y) holds

for i, A being set st i in X holds

((commute f) . i) .: A = pi ((f .: A),i)

proof end;

theorem Th9: :: WAYBEL27:9

for f being Function

for i, A being set st [:A,{i}:] c= dom f holds

pi (((curry f) .: A),i) = f .: [:A,{i}:]

for i, A being set st [:A,{i}:] c= dom f holds

pi (((curry f) .: A),i) = f .: [:A,{i}:]

proof end;

registration
end;

registration

ex b_{1} being LATTICE st

( b_{1} is constituted-Functions & b_{1} is complete & b_{1} is strict )

ex b_{1} being 1-sorted st

( b_{1} is constituted-Functions & not b_{1} is empty )
end;

cluster non empty constituted-Functions strict reflexive transitive antisymmetric V226() V227() complete non void for RelStr ;

existence ex b

( b

proof end;

existence ex b

( b

proof end;

registration

let T be non empty constituted-Functions RelStr ;

coherence

for b_{1} being non empty SubRelStr of T holds b_{1} is constituted-Functions

end;
coherence

for b

proof end;

theorem Th10: :: WAYBEL27:10

for S, T being complete LATTICE

for f being idempotent Function of T,T

for h being Function of S,(Image f) holds f * h = h

for f being idempotent Function of T,T

for h being Function of S,(Image f) holds f * h = h

proof end;

theorem :: WAYBEL27:11

for S, T, T1 being non empty RelStr st T is SubRelStr of T1 holds

for f being Function of S,T

for f1 being Function of S,T1 st f is monotone & f = f1 holds

f1 is monotone

for f being Function of S,T

for f1 being Function of S,T1 st f is monotone & f = f1 holds

f1 is monotone

proof end;

theorem Th12: :: WAYBEL27:12

for S, T, T1 being non empty RelStr st T is full SubRelStr of T1 holds

for f being Function of S,T

for f1 being Function of S,T1 st f1 is monotone & f = f1 holds

f is monotone

for f being Function of S,T

for f1 being Function of S,T1 st f1 is monotone & f = f1 holds

f is monotone

proof end;

definition

let X be non empty set ;

let T be non empty RelStr ;

let f be Element of (T |^ X);

let x be Element of X;

:: original: .

redefine func f . x -> Element of T;

coherence

f . x is Element of T

end;
let T be non empty RelStr ;

let f be Element of (T |^ X);

let x be Element of X;

:: original: .

redefine func f . x -> Element of T;

coherence

f . x is Element of T

proof end;

theorem Th14: :: WAYBEL27:14

for X being non empty set

for T being non empty RelStr

for f, g being Element of (T |^ X) holds

( f <= g iff for x being Element of X holds f . x <= g . x )

for T being non empty RelStr

for f, g being Element of (T |^ X) holds

( f <= g iff for x being Element of X holds f . x <= g . x )

proof end;

theorem Th15: :: WAYBEL27:15

for X being set

for L, S being non empty RelStr st RelStr(# the carrier of L, the InternalRel of L #) = RelStr(# the carrier of S, the InternalRel of S #) holds

L |^ X = S |^ X

for L, S being non empty RelStr st RelStr(# the carrier of L, the InternalRel of L #) = RelStr(# the carrier of S, the InternalRel of S #) holds

L |^ X = S |^ X

proof end;

theorem :: WAYBEL27:16

for S1, S2, T1, T2 being non empty TopSpace st TopStruct(# the carrier of S1, the topology of S1 #) = TopStruct(# the carrier of S2, the topology of S2 #) & TopStruct(# the carrier of T1, the topology of T1 #) = TopStruct(# the carrier of T2, the topology of T2 #) holds

oContMaps (S1,T1) = oContMaps (S2,T2)

oContMaps (S1,T1) = oContMaps (S2,T2)

proof end;

theorem Th17: :: WAYBEL27:17

for X being set ex f being Function of (BoolePoset X),((BoolePoset {0}) |^ X) st

( f is isomorphic & ( for Y being Subset of X holds f . Y = chi (Y,X) ) )

( f is isomorphic & ( for Y being Subset of X holds f . Y = chi (Y,X) ) )

proof end;

theorem Th19: :: WAYBEL27:19

for X, Y being non empty set

for T being non empty Poset

for S1 being non empty full SubRelStr of (T |^ X) |^ Y

for S2 being non empty full SubRelStr of (T |^ Y) |^ X

for F being Function of S1,S2 st F is commuting holds

F is monotone

for T being non empty Poset

for S1 being non empty full SubRelStr of (T |^ X) |^ Y

for S2 being non empty full SubRelStr of (T |^ Y) |^ X

for F being Function of S1,S2 st F is commuting holds

F is monotone

proof end;

theorem Th20: :: WAYBEL27:20

for X, Y being non empty set

for T being non empty Poset

for S1 being non empty full SubRelStr of (T |^ Y) |^ X

for S2 being non empty full SubRelStr of T |^ [:X,Y:]

for F being Function of S1,S2 st F is uncurrying holds

F is monotone

for T being non empty Poset

for S1 being non empty full SubRelStr of (T |^ Y) |^ X

for S2 being non empty full SubRelStr of T |^ [:X,Y:]

for F being Function of S1,S2 st F is uncurrying holds

F is monotone

proof end;

theorem Th21: :: WAYBEL27:21

for X, Y being non empty set

for T being non empty Poset

for S1 being non empty full SubRelStr of (T |^ Y) |^ X

for S2 being non empty full SubRelStr of T |^ [:X,Y:]

for F being Function of S2,S1 st F is currying holds

F is monotone

for T being non empty Poset

for S1 being non empty full SubRelStr of (T |^ Y) |^ X

for S2 being non empty full SubRelStr of T |^ [:X,Y:]

for F being Function of S2,S1 st F is currying holds

F is monotone

proof end;

definition

let S be non empty RelStr ;

let T be non empty reflexive antisymmetric RelStr ;

ex b_{1} being strict RelStr st

( b_{1} is full SubRelStr of T |^ the carrier of S & ( for x being set holds

( x in the carrier of b_{1} iff x is directed-sups-preserving Function of S,T ) ) )

for b_{1}, b_{2} being strict RelStr st b_{1} is full SubRelStr of T |^ the carrier of S & ( for x being set holds

( x in the carrier of b_{1} iff x is directed-sups-preserving Function of S,T ) ) & b_{2} is full SubRelStr of T |^ the carrier of S & ( for x being set holds

( x in the carrier of b_{2} iff x is directed-sups-preserving Function of S,T ) ) holds

b_{1} = b_{2}

end;
let T be non empty reflexive antisymmetric RelStr ;

func UPS (S,T) -> strict RelStr means :Def4: :: WAYBEL27:def 4

( it is full SubRelStr of T |^ the carrier of S & ( for x being set holds

( x in the carrier of it iff x is directed-sups-preserving Function of S,T ) ) );

existence ( it is full SubRelStr of T |^ the carrier of S & ( for x being set holds

( x in the carrier of it iff x is directed-sups-preserving Function of S,T ) ) );

ex b

( b

( x in the carrier of b

proof end;

uniqueness for b

( x in the carrier of b

( x in the carrier of b

b

proof end;

:: deftheorem Def4 defines UPS WAYBEL27:def 4 :

for S being non empty RelStr

for T being non empty reflexive antisymmetric RelStr

for b_{3} being strict RelStr holds

( b_{3} = UPS (S,T) iff ( b_{3} is full SubRelStr of T |^ the carrier of S & ( for x being set holds

( x in the carrier of b_{3} iff x is directed-sups-preserving Function of S,T ) ) ) );

for S being non empty RelStr

for T being non empty reflexive antisymmetric RelStr

for b

( b

( x in the carrier of b

registration

let S be non empty RelStr ;

let T be non empty reflexive antisymmetric RelStr ;

coherence

( not UPS (S,T) is empty & UPS (S,T) is reflexive & UPS (S,T) is antisymmetric & UPS (S,T) is constituted-Functions )

end;
let T be non empty reflexive antisymmetric RelStr ;

coherence

( not UPS (S,T) is empty & UPS (S,T) is reflexive & UPS (S,T) is antisymmetric & UPS (S,T) is constituted-Functions )

proof end;

registration
end;

theorem Th22: :: WAYBEL27:22

for S being non empty RelStr

for T being non empty reflexive antisymmetric RelStr holds the carrier of (UPS (S,T)) c= Funcs ( the carrier of S, the carrier of T)

for T being non empty reflexive antisymmetric RelStr holds the carrier of (UPS (S,T)) c= Funcs ( the carrier of S, the carrier of T)

proof end;

definition

let S be non empty RelStr ;

let T be non empty reflexive antisymmetric RelStr ;

let f be Element of (UPS (S,T));

let s be Element of S;

:: original: .

redefine func f . s -> Element of T;

coherence

f . s is Element of T

end;
let T be non empty reflexive antisymmetric RelStr ;

let f be Element of (UPS (S,T));

let s be Element of S;

:: original: .

redefine func f . s -> Element of T;

coherence

f . s is Element of T

proof end;

theorem Th23: :: WAYBEL27:23

for S being non empty RelStr

for T being non empty reflexive antisymmetric RelStr

for f, g being Element of (UPS (S,T)) holds

( f <= g iff for s being Element of S holds f . s <= g . s )

for T being non empty reflexive antisymmetric RelStr

for f, g being Element of (UPS (S,T)) holds

( f <= g iff for s being Element of S holds f . s <= g . s )

proof end;

theorem Th25: :: WAYBEL27:25

for S, S9 being non empty RelStr

for T, T9 being non empty reflexive antisymmetric RelStr st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of S9, the InternalRel of S9 #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of T9, the InternalRel of T9 #) holds

UPS (S,T) = UPS (S9,T9)

for T, T9 being non empty reflexive antisymmetric RelStr st RelStr(# the carrier of S, the InternalRel of S #) = RelStr(# the carrier of S9, the InternalRel of S9 #) & RelStr(# the carrier of T, the InternalRel of T #) = RelStr(# the carrier of T9, the InternalRel of T9 #) holds

UPS (S,T) = UPS (S9,T9)

proof end;

theorem Th26: :: WAYBEL27:26

for S, T being complete LATTICE holds UPS (S,T) is sups-inheriting SubRelStr of T |^ the carrier of S

proof end;

theorem Th27: :: WAYBEL27:27

for S, T being complete LATTICE

for A being Subset of (UPS (S,T)) holds sup A = "\/" (A,(T |^ the carrier of S))

for A being Subset of (UPS (S,T)) holds sup A = "\/" (A,(T |^ the carrier of S))

proof end;

definition

let S1, S2, T1, T2 be non empty reflexive antisymmetric RelStr ;

let f be Function of S1,S2;

assume A1: f is directed-sups-preserving ;

let g be Function of T1,T2;

assume A2: g is directed-sups-preserving ;

ex b_{1} being Function of (UPS (S2,T1)),(UPS (S1,T2)) st

for h being directed-sups-preserving Function of S2,T1 holds b_{1} . h = (g * h) * f

for b_{1}, b_{2} being Function of (UPS (S2,T1)),(UPS (S1,T2)) st ( for h being directed-sups-preserving Function of S2,T1 holds b_{1} . h = (g * h) * f ) & ( for h being directed-sups-preserving Function of S2,T1 holds b_{2} . h = (g * h) * f ) holds

b_{1} = b_{2}

end;
let f be Function of S1,S2;

assume A1: f is directed-sups-preserving ;

let g be Function of T1,T2;

assume A2: g is directed-sups-preserving ;

func UPS (f,g) -> Function of (UPS (S2,T1)),(UPS (S1,T2)) means :Def5: :: WAYBEL27:def 5

for h being directed-sups-preserving Function of S2,T1 holds it . h = (g * h) * f;

existence for h being directed-sups-preserving Function of S2,T1 holds it . h = (g * h) * f;

ex b

for h being directed-sups-preserving Function of S2,T1 holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines UPS WAYBEL27:def 5 :

for S1, S2, T1, T2 being non empty reflexive antisymmetric RelStr

for f being Function of S1,S2 st f is directed-sups-preserving holds

for g being Function of T1,T2 st g is directed-sups-preserving holds

for b_{7} being Function of (UPS (S2,T1)),(UPS (S1,T2)) holds

( b_{7} = UPS (f,g) iff for h being directed-sups-preserving Function of S2,T1 holds b_{7} . h = (g * h) * f );

for S1, S2, T1, T2 being non empty reflexive antisymmetric RelStr

for f being Function of S1,S2 st f is directed-sups-preserving holds

for g being Function of T1,T2 st g is directed-sups-preserving holds

for b

( b

theorem Th28: :: WAYBEL27:28

for S1, S2, S3, T1, T2, T3 being non empty Poset

for f1 being directed-sups-preserving Function of S2,S3

for f2 being directed-sups-preserving Function of S1,S2

for g1 being directed-sups-preserving Function of T1,T2

for g2 being directed-sups-preserving Function of T2,T3 holds (UPS (f2,g2)) * (UPS (f1,g1)) = UPS ((f1 * f2),(g2 * g1))

for f1 being directed-sups-preserving Function of S2,S3

for f2 being directed-sups-preserving Function of S1,S2

for g1 being directed-sups-preserving Function of T1,T2

for g2 being directed-sups-preserving Function of T2,T3 holds (UPS (f2,g2)) * (UPS (f1,g1)) = UPS ((f1 * f2),(g2 * g1))

proof end;

:: 2.6. PROPOSITOION, p. 115

:: preservation of identities

:: preservation of identities

:: 2.6. PROPOSITOION, p. 115

:: preservation of directed-sups

:: preservation of directed-sups

theorem Th30: :: WAYBEL27:30

for S1, S2, T1, T2 being complete LATTICE

for f being directed-sups-preserving Function of S1,S2

for g being directed-sups-preserving Function of T1,T2 holds UPS (f,g) is directed-sups-preserving

for f being directed-sups-preserving Function of S1,S2

for g being directed-sups-preserving Function of T1,T2 holds UPS (f,g) is directed-sups-preserving

proof end;

theorem :: WAYBEL27:32

for S being complete Scott TopLattice holds oContMaps (S,Sierpinski_Space) = UPS (S,(BoolePoset {0}))

proof end;

:: 2.7. LEMMA, p. 116

theorem Th33: :: WAYBEL27:33

for S being complete LATTICE ex F being Function of (UPS (S,(BoolePoset {0}))),(InclPoset (sigma S)) st

( F is isomorphic & ( for f being directed-sups-preserving Function of S,(BoolePoset {0}) holds F . f = f " {1} ) )

( F is isomorphic & ( for f being directed-sups-preserving Function of S,(BoolePoset {0}) holds F . f = f " {1} ) )

proof end;

theorem Th35: :: WAYBEL27:35

for S1, S2, T1, T2 being complete LATTICE

for f being Function of S1,S2

for g being Function of T1,T2 st f is isomorphic & g is isomorphic holds

UPS (f,g) is isomorphic

for f being Function of S1,S2

for g being Function of T1,T2 st f is isomorphic & g is isomorphic holds

UPS (f,g) is isomorphic

proof end;

theorem Th36: :: WAYBEL27:36

for S1, S2, T1, T2 being complete LATTICE st S1,S2 are_isomorphic & T1,T2 are_isomorphic holds

UPS (S2,T1), UPS (S1,T2) are_isomorphic

UPS (S2,T1), UPS (S1,T2) are_isomorphic

proof end;

theorem Th37: :: WAYBEL27:37

for S, T being complete LATTICE

for f being directed-sups-preserving projection Function of T,T holds Image (UPS ((id S),f)) = UPS (S,(Image f))

for f being directed-sups-preserving projection Function of T,T holds Image (UPS ((id S),f)) = UPS (S,(Image f))

proof end;

Lm1: now :: thesis: for M being non empty set

for X, Y being non empty Poset

for f being directed-sups-preserving Function of X,(Y |^ M) holds

( f in Funcs ( the carrier of X,(Funcs (M, the carrier of Y))) & rng (commute f) c= Funcs ( the carrier of X, the carrier of Y) & dom (commute f) = M )

for X, Y being non empty Poset

for f being directed-sups-preserving Function of X,(Y |^ M) holds

( f in Funcs ( the carrier of X,(Funcs (M, the carrier of Y))) & rng (commute f) c= Funcs ( the carrier of X, the carrier of Y) & dom (commute f) = M )

let M be non empty set ; :: thesis: for X, Y being non empty Poset

for f being directed-sups-preserving Function of X,(Y |^ M) holds

( f in Funcs ( the carrier of X,(Funcs (M, the carrier of Y))) & rng (commute f) c= Funcs ( the carrier of X, the carrier of Y) & dom (commute f) = M )

let X, Y be non empty Poset; :: thesis: for f being directed-sups-preserving Function of X,(Y |^ M) holds

( f in Funcs ( the carrier of X,(Funcs (M, the carrier of Y))) & rng (commute f) c= Funcs ( the carrier of X, the carrier of Y) & dom (commute f) = M )

let f be directed-sups-preserving Function of X,(Y |^ M); :: thesis: ( f in Funcs ( the carrier of X,(Funcs (M, the carrier of Y))) & rng (commute f) c= Funcs ( the carrier of X, the carrier of Y) & dom (commute f) = M )

the carrier of (Y |^ M) = Funcs (M, the carrier of Y) by YELLOW_1:28;

then A1: rng f c= Funcs (M, the carrier of Y) ;

dom f = the carrier of X by FUNCT_2:def 1;

hence f in Funcs ( the carrier of X,(Funcs (M, the carrier of Y))) by A1, FUNCT_2:def 2; :: thesis: ( rng (commute f) c= Funcs ( the carrier of X, the carrier of Y) & dom (commute f) = M )

then commute f in Funcs (M,(Funcs ( the carrier of X, the carrier of Y))) by FUNCT_6:55;

then ex g being Function st

( commute f = g & dom g = M & rng g c= Funcs ( the carrier of X, the carrier of Y) ) by FUNCT_2:def 2;

hence ( rng (commute f) c= Funcs ( the carrier of X, the carrier of Y) & dom (commute f) = M ) ; :: thesis: verum

end;
for f being directed-sups-preserving Function of X,(Y |^ M) holds

( f in Funcs ( the carrier of X,(Funcs (M, the carrier of Y))) & rng (commute f) c= Funcs ( the carrier of X, the carrier of Y) & dom (commute f) = M )

let X, Y be non empty Poset; :: thesis: for f being directed-sups-preserving Function of X,(Y |^ M) holds

( f in Funcs ( the carrier of X,(Funcs (M, the carrier of Y))) & rng (commute f) c= Funcs ( the carrier of X, the carrier of Y) & dom (commute f) = M )

let f be directed-sups-preserving Function of X,(Y |^ M); :: thesis: ( f in Funcs ( the carrier of X,(Funcs (M, the carrier of Y))) & rng (commute f) c= Funcs ( the carrier of X, the carrier of Y) & dom (commute f) = M )

the carrier of (Y |^ M) = Funcs (M, the carrier of Y) by YELLOW_1:28;

then A1: rng f c= Funcs (M, the carrier of Y) ;

dom f = the carrier of X by FUNCT_2:def 1;

hence f in Funcs ( the carrier of X,(Funcs (M, the carrier of Y))) by A1, FUNCT_2:def 2; :: thesis: ( rng (commute f) c= Funcs ( the carrier of X, the carrier of Y) & dom (commute f) = M )

then commute f in Funcs (M,(Funcs ( the carrier of X, the carrier of Y))) by FUNCT_6:55;

then ex g being Function st

( commute f = g & dom g = M & rng g c= Funcs ( the carrier of X, the carrier of Y) ) by FUNCT_2:def 2;

hence ( rng (commute f) c= Funcs ( the carrier of X, the carrier of Y) & dom (commute f) = M ) ; :: thesis: verum

theorem Th38: :: WAYBEL27:38

for X being non empty set

for S, T being non empty Poset

for f being directed-sups-preserving Function of S,(T |^ X)

for i being Element of X holds (commute f) . i is directed-sups-preserving Function of S,T

for S, T being non empty Poset

for f being directed-sups-preserving Function of S,(T |^ X)

for i being Element of X holds (commute f) . i is directed-sups-preserving Function of S,T

proof end;

theorem Th39: :: WAYBEL27:39

for X being non empty set

for S, T being non empty Poset

for f being directed-sups-preserving Function of S,(T |^ X) holds commute f is Function of X, the carrier of (UPS (S,T))

for S, T being non empty Poset

for f being directed-sups-preserving Function of S,(T |^ X) holds commute f is Function of X, the carrier of (UPS (S,T))

proof end;

theorem Th40: :: WAYBEL27:40

for X being non empty set

for S, T being non empty Poset

for f being Function of X, the carrier of (UPS (S,T)) holds commute f is directed-sups-preserving Function of S,(T |^ X)

for S, T being non empty Poset

for f being Function of X, the carrier of (UPS (S,T)) holds commute f is directed-sups-preserving Function of S,(T |^ X)

proof end;

theorem Th41: :: WAYBEL27:41

for X being non empty set

for S, T being non empty Poset ex F being Function of (UPS (S,(T |^ X))),((UPS (S,T)) |^ X) st

( F is commuting & F is isomorphic )

for S, T being non empty Poset ex F being Function of (UPS (S,(T |^ X))),((UPS (S,T)) |^ X) st

( F is commuting & F is isomorphic )

proof end;

theorem Th42: :: WAYBEL27:42

for X being non empty set

for S, T being non empty Poset holds UPS (S,(T |^ X)),(UPS (S,T)) |^ X are_isomorphic

for S, T being non empty Poset holds UPS (S,(T |^ X)),(UPS (S,T)) |^ X are_isomorphic

proof end;

:: 2.8. THEOREM, p. 116

:: [CONT -> CONT] is into CONT (so [CONT -> CONT] is functor)

:: [CONT -> CONT] is into CONT (so [CONT -> CONT] is functor)

:: 2.8. THEOREM, p. 116

:: [ALG -> ALG] is into ALG (so [ALG -> ALG] is functor)

:: [ALG -> ALG] is into ALG (so [ALG -> ALG] is functor)

theorem Th45: :: WAYBEL27:45

for R, S, T being complete LATTICE

for f being directed-sups-preserving Function of R,(UPS (S,T)) holds uncurry f is directed-sups-preserving Function of [:R,S:],T

for f being directed-sups-preserving Function of R,(UPS (S,T)) holds uncurry f is directed-sups-preserving Function of [:R,S:],T

proof end;

theorem Th46: :: WAYBEL27:46

for R, S, T being complete LATTICE

for f being directed-sups-preserving Function of [:R,S:],T holds curry f is directed-sups-preserving Function of R,(UPS (S,T))

for f being directed-sups-preserving Function of [:R,S:],T holds curry f is directed-sups-preserving Function of R,(UPS (S,T))

proof end;

:: 2.10. THEOREM, p. 117

theorem :: WAYBEL27:47

for R, S, T being complete LATTICE ex f being Function of (UPS (R,(UPS (S,T)))),(UPS ([:R,S:],T)) st

( f is uncurrying & f is isomorphic )

( f is uncurrying & f is isomorphic )

proof end;

:: preservation of composition