let S, T be complete Scott TopLattice; :: thesis: for f being Function of S,T st S is algebraic & T is algebraic & ( for x being Element of S

for y being Element of T holds

( y << f . x iff ex w being Element of S st

( w << x & y << f . w ) ) ) holds

for x being Element of S

for k being Element of T st k in the carrier of (CompactSublatt T) holds

( k <= f . x iff ex j being Element of S st

( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) )

let f be Function of S,T; :: thesis: ( S is algebraic & T is algebraic & ( for x being Element of S

for y being Element of T holds

( y << f . x iff ex w being Element of S st

( w << x & y << f . w ) ) ) implies for x being Element of S

for k being Element of T st k in the carrier of (CompactSublatt T) holds

( k <= f . x iff ex j being Element of S st

( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) )

assume that

A1: S is algebraic and

A2: T is algebraic ; :: thesis: ( ex x being Element of S ex y being Element of T st

( ( y << f . x implies ex w being Element of S st

( w << x & y << f . w ) ) implies ( ex w being Element of S st

( w << x & y << f . w ) & not y << f . x ) ) or for x being Element of S

for k being Element of T st k in the carrier of (CompactSublatt T) holds

( k <= f . x iff ex j being Element of S st

( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) )

A3: S is continuous by A1, WAYBEL_8:7;

A4: T is continuous by A2, WAYBEL_8:7;

assume A5: for x being Element of S

for y being Element of T holds

( y << f . x iff ex w being Element of S st

( w << x & y << f . w ) ) ; :: thesis: for x being Element of S

for k being Element of T st k in the carrier of (CompactSublatt T) holds

( k <= f . x iff ex j being Element of S st

( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) )

then A6: f is continuous by A3, A4, Th23;

let x be Element of S; :: thesis: for k being Element of T st k in the carrier of (CompactSublatt T) holds

( k <= f . x iff ex j being Element of S st

( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) )

let k be Element of T; :: thesis: ( k in the carrier of (CompactSublatt T) implies ( k <= f . x iff ex j being Element of S st

( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) )

assume A7: k in the carrier of (CompactSublatt T) ; :: thesis: ( k <= f . x iff ex j being Element of S st

( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) )

A14: j <= x and

A15: k <= f . j ; :: thesis: k <= f . x

f is continuous by A3, A4, A5, Lm15;

then f . j <= f . x by A14, WAYBEL_1:def 2;

hence k <= f . x by A15, ORDERS_2:3; :: thesis: verum

for y being Element of T holds

( y << f . x iff ex w being Element of S st

( w << x & y << f . w ) ) ) holds

for x being Element of S

for k being Element of T st k in the carrier of (CompactSublatt T) holds

( k <= f . x iff ex j being Element of S st

( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) )

let f be Function of S,T; :: thesis: ( S is algebraic & T is algebraic & ( for x being Element of S

for y being Element of T holds

( y << f . x iff ex w being Element of S st

( w << x & y << f . w ) ) ) implies for x being Element of S

for k being Element of T st k in the carrier of (CompactSublatt T) holds

( k <= f . x iff ex j being Element of S st

( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) )

assume that

A1: S is algebraic and

A2: T is algebraic ; :: thesis: ( ex x being Element of S ex y being Element of T st

( ( y << f . x implies ex w being Element of S st

( w << x & y << f . w ) ) implies ( ex w being Element of S st

( w << x & y << f . w ) & not y << f . x ) ) or for x being Element of S

for k being Element of T st k in the carrier of (CompactSublatt T) holds

( k <= f . x iff ex j being Element of S st

( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) )

A3: S is continuous by A1, WAYBEL_8:7;

A4: T is continuous by A2, WAYBEL_8:7;

assume A5: for x being Element of S

for y being Element of T holds

( y << f . x iff ex w being Element of S st

( w << x & y << f . w ) ) ; :: thesis: for x being Element of S

for k being Element of T st k in the carrier of (CompactSublatt T) holds

( k <= f . x iff ex j being Element of S st

( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) )

then A6: f is continuous by A3, A4, Th23;

let x be Element of S; :: thesis: for k being Element of T st k in the carrier of (CompactSublatt T) holds

( k <= f . x iff ex j being Element of S st

( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) )

let k be Element of T; :: thesis: ( k in the carrier of (CompactSublatt T) implies ( k <= f . x iff ex j being Element of S st

( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) )

assume A7: k in the carrier of (CompactSublatt T) ; :: thesis: ( k <= f . x iff ex j being Element of S st

( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) )

hereby :: thesis: ( ex j being Element of S st

( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) implies k <= f . x )

given j being Element of S such that
j in the carrier of (CompactSublatt S)
and ( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) implies k <= f . x )

assume
k <= f . x
; :: thesis: ex w1 being Element of S st

( w1 in the carrier of (CompactSublatt S) & w1 <= x & k <= f . w1 )

then k << f . x by A7, WAYBEL_8:1;

then consider w being Element of S such that

A8: w << x and

A9: k << f . w by A5;

consider w1 being Element of S such that

A10: w1 in the carrier of (CompactSublatt S) and

A11: w <= w1 and

A12: w1 <= x by A1, A8, WAYBEL_8:7;

A13: k <= f . w by A9, WAYBEL_3:1;

take w1 = w1; :: thesis: ( w1 in the carrier of (CompactSublatt S) & w1 <= x & k <= f . w1 )

thus w1 in the carrier of (CompactSublatt S) by A10; :: thesis: ( w1 <= x & k <= f . w1 )

thus w1 <= x by A12; :: thesis: k <= f . w1

f . w <= f . w1 by A6, A11, WAYBEL_1:def 2;

hence k <= f . w1 by A13, ORDERS_2:3; :: thesis: verum

end;( w1 in the carrier of (CompactSublatt S) & w1 <= x & k <= f . w1 )

then k << f . x by A7, WAYBEL_8:1;

then consider w being Element of S such that

A8: w << x and

A9: k << f . w by A5;

consider w1 being Element of S such that

A10: w1 in the carrier of (CompactSublatt S) and

A11: w <= w1 and

A12: w1 <= x by A1, A8, WAYBEL_8:7;

A13: k <= f . w by A9, WAYBEL_3:1;

take w1 = w1; :: thesis: ( w1 in the carrier of (CompactSublatt S) & w1 <= x & k <= f . w1 )

thus w1 in the carrier of (CompactSublatt S) by A10; :: thesis: ( w1 <= x & k <= f . w1 )

thus w1 <= x by A12; :: thesis: k <= f . w1

f . w <= f . w1 by A6, A11, WAYBEL_1:def 2;

hence k <= f . w1 by A13, ORDERS_2:3; :: thesis: verum

A14: j <= x and

A15: k <= f . j ; :: thesis: k <= f . x

f is continuous by A3, A4, A5, Lm15;

then f . j <= f . x by A14, WAYBEL_1:def 2;

hence k <= f . x by A15, ORDERS_2:3; :: thesis: verum