let S, T be complete Scott TopLattice; for f being Function of S,T st T is algebraic & ( 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 ) ) ) holds
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 ) )
let f be Function of S,T; ( T is algebraic & ( 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 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 ) ) )
assume A1:
T is algebraic
; ( ex x being Element of S ex k being Element of T st
( k in the carrier of (CompactSublatt T) & not ( k <= f . x iff ex j being Element of S st
( j in the carrier of (CompactSublatt S) & j <= x & k <= f . j ) ) ) or 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 ) ) )
assume A2:
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 ) )
; 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 ) )
let x be 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 ) )
let y be Element of T; ( y << f . x iff ex w being Element of S st
( w << x & y << f . w ) )
hereby ( ex w being Element of S st
( w << x & y << f . w ) implies y << f . x )
end;
given w being Element of S such that A9:
w << x
and
A10:
y << f . w
; y << f . x
consider h being Element of T such that
A11:
h in the carrier of (CompactSublatt T)
and
A12:
y <= h
and
A13:
h <= f . w
by A1, A10, WAYBEL_8:7;
consider j being Element of S such that
A14:
j in the carrier of (CompactSublatt S)
and
A15:
j <= w
and
A16:
h <= f . j
by A2, A11, A13;
j << x
by A9, A15, WAYBEL_3:2;
then
j <= x
by WAYBEL_3:1;
then
h <= f . x
by A2, A11, A14, A16;
hence
y << f . x
by A11, A12, WAYBEL_8:1; verum