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

( f is continuous iff 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 implies ( f is continuous iff 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: ( f is continuous iff 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;

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 ) ) ; :: thesis: f is continuous

then 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 ) ) by A2, Lm18;

hence f is continuous by A3, A4, Th23; :: thesis: verum

( f is continuous iff 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 implies ( f is continuous iff 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: ( f is continuous iff 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;

hereby :: 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 ) ) ) implies f is continuous )

assume
for x being Element of Sfor 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 ) ) ) implies f is continuous )

assume
f is continuous
; :: 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 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 ) ) by A3, A4, Th23;

hence 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 ) ) by A1, A2, Lm17; :: thesis: verum

end;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 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 ) ) by A3, A4, Th23;

hence 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 ) ) by A1, A2, Lm17; :: thesis: verum

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 ) ) ; :: thesis: f is continuous

then 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 ) ) by A2, Lm18;

hence f is continuous by A3, A4, Th23; :: thesis: verum