let I be non empty set ; :: thesis: for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of st ( for i being Element of I holds J . i is complete continuous LATTICE ) holds
product J is continuous
let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of ; :: thesis: ( ( for i being Element of I holds J . i is complete continuous LATTICE ) implies product J is continuous )
assume A1: for i being Element of I holds J . i is complete continuous LATTICE ; :: thesis: product J is continuous
A2: for i being Element of I holds J . i is complete LATTICE by A1;
set pJ = product J;
reconsider pJ' = product J as complete LATTICE by A2, WAYBEL_3:31;

hereby :: according to WAYBEL_3:def 6 :: thesis: ( product J is up-complete & product J is satisfying_axiom_of_approximation )

let x be Element of (product J); :: thesis: ( not waybelow x is empty & waybelow x is directed )
reconsider x' = x as Element of pJ' ;
not waybelow x' is empty ;
hence not waybelow x is empty ; :: thesis: waybelow x is directed
waybelow x' is directed ;
hence waybelow x is directed ; :: thesis: verum

end;

pJ' is up-complete ;
hence product J is up-complete ; :: thesis: product J is satisfying_axiom_of_approximation
let x be Element of (product J); :: according to WAYBEL_3:def 5 :: thesis: x = "\/" (waybelow x),(product J)
set swx = sup (waybelow x);

now

thus dom x = I by WAYBEL_3:27; :: thesis: ( dom (sup (waybelow x)) = I & ( for i being set st i in I holds
x . i = (sup (waybelow x)) . i ) )
thus dom (sup (waybelow x)) = I by WAYBEL_3:27; :: thesis: for i being set st i in I holds
x . i = (sup (waybelow x)) . i
let i be set ; :: thesis: ( i in I implies x . i = (sup (waybelow x)) . i )
assume i in I ; :: thesis: x . i = (sup (waybelow x)) . i
then reconsider i' = i as Element of I ;

now

reconsider K = {i'} as finite Subset of I ;
deffunc H₁( Element of I) -> Element of the carrier of (J . $1) = Bottom (J . $1);
let a be set ; :: thesis: ( ( a in pi (waybelow x),i' implies a in waybelow (x . i') ) & ( a in waybelow (x . i') implies a in pi (waybelow x),i' ) )
consider g being ManySortedSet of such that
A3: for i being Element of I holds g . i = H₁(i) from PBOOLE:sch 5();
set f = g +* i,a;

hereby :: thesis: ( a in waybelow (x . i') implies a in pi (waybelow x),i' )

assume a in pi (waybelow x),i' ; :: thesis: a in waybelow (x . i')
then consider f being Function such that
A4: f in waybelow x and
A5: a = f . i by CARD_3:def 6;
reconsider f = f as Element of (product J) by A4;
f << x by A4, WAYBEL_3:7;
then f . i' << x . i' by A2, WAYBEL_3:33;
hence a in waybelow (x . i') by A5; :: thesis: verum

end;

A6: dom g = I by PARTFUN1:def 4;
then A7: dom (g +* i,a) = I by FUNCT_7:32;
assume A8: a in waybelow (x . i') ; :: thesis: a in pi (waybelow x),i'

now

let j be Element of I; :: thesis: (g +* i,a) . b₁ is Element of (J . b₁)

per cases ( i' = j or i' <> j ) ;

suppose i' = j ; :: thesis: (g +* i,a) . b₁ is Element of (J . b₁)

hence (g +* i,a) . j is Element of (J . j) by A8, A6, FUNCT_7:33; :: thesis: verum

end;

suppose i' <> j ; :: thesis: (g +* i,a) . b₁ is Element of (J . b₁)

then (g +* i,a) . j = g . j by FUNCT_7:34
.= Bottom (J . j) by A3 ;
hence (g +* i,a) . j is Element of (J . j) ; :: thesis: verum

end;

end;

end;

then reconsider f = g +* i,a as Element of (product J) by A7, WAYBEL_3:27;

A9: now

let j be Element of I; :: thesis: f . b₁ << x . b₁

per cases ( i' = j or i' <> j ) ;

suppose A10: i' = j ; :: thesis: f . b₁ << x . b₁

f . i' = a by A6, FUNCT_7:33;
hence f . j << x . j by A8, A10, WAYBEL_3:7; :: thesis: verum

end;

suppose A11: i' <> j ; :: thesis: f . b₁ << x . b₁

A12: J . j is complete LATTICE by A1;
f . j = g . j by A11, FUNCT_7:34
.= Bottom (J . j) by A3 ;
hence f . j << x . j by A12, WAYBEL_3:4; :: thesis: verum

end;

end;

end;

now

let j be Element of I; :: thesis: ( not j in K implies f . j = Bottom (J . j) )
assume not j in K ; :: thesis: f . j = Bottom (J . j)
then j <> i' by TARSKI:def 1;
hence f . j = g . j by FUNCT_7:34
.= Bottom (J . j) by A3 ;
:: thesis: verum

end;

then f << x by A2, A9, WAYBEL_3:33;
then A13: f in waybelow x ;
a = f . i' by A6, FUNCT_7:33;
hence a in pi (waybelow x),i' by A13, CARD_3:def 6; :: thesis: verum

end;

then A14: pi (waybelow x),i' = waybelow (x . i') by TARSKI:2;
( (sup (waybelow x)) . i' = sup (pi (waybelow x),i') & J . i' is satisfying_axiom_of_approximation ) by A1, A2, WAYBEL_3:32;
hence x . i = (sup (waybelow x)) . i by A14, WAYBEL_3:def 5; :: thesis: verum

end;

hence x = "\/" (waybelow x),(product J) by FUNCT_1:9; :: thesis: verum