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
set pJ = product J;
A2: for i being Element of I holds J . i is complete LATTICE by A1;
then reconsider pJ' = product J as complete LATTICE by 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 ;
A3: (sup (waybelow x)) . i' = sup (pi (waybelow x),i') by A2, WAYBEL_3:32;

now

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' ) )

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;

assume A6: a in waybelow (x . i') ; :: thesis: a in pi (waybelow x),i'
deffunc H₁( Element of I) -> Element of the carrier of (J . $1) = Bottom (J . $1);
consider g being ManySortedSet of such that
A7: for i being Element of I holds g . i = H₁(i) from PBOOLE:sch 5();
A8: dom g = I by PARTFUN1:def 4;
set f = g +* i,a;
A9: dom (g +* i,a) = I by A8, FUNCT_7:32;

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 A6, A8, 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 A7 ;
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 A9, WAYBEL_3:27;

A10: now

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

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

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

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

end;

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

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

end;

end;

end;

reconsider K = {i'} as finite Subset of I ;

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 A7 ;
:: thesis: verum

end;

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

end;

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

end;

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