let I be non empty set ; :: thesis: for J being RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I 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 I; :: 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 pJ9 = 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 x9 = x as Element of pJ9 ;
not waybelow x9 is empty ;
hence not waybelow x is empty ; :: thesis: waybelow x is directed
waybelow x9 is directed ;
hence waybelow x is directed ; :: thesis: verum

end;

pJ9 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 :: thesis: ( dom x = I & dom (sup (waybelow x)) = I & ( for i being object st i in I holds
x . i = (sup (waybelow x)) . i ) )

thus dom x = I by WAYBEL_3:27; :: thesis: ( dom (sup (waybelow x)) = I & ( for i being object 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 object st i in I holds
x . i = (sup (waybelow x)) . i
let i be object ; :: thesis: ( i in I implies x . i = (sup (waybelow x)) . i )
assume i in I ; :: thesis: x . i = (sup (waybelow x)) . i
then reconsider i9 = i as Element of I ;

now :: thesis: for a being object holds
( ( a in pi ((waybelow x),i9) implies a in waybelow (x . i9) ) & ( a in waybelow (x . i9) implies a in pi ((waybelow x),i9) ) )

reconsider K = {i9} as finite Subset of I ;
deffunc H₁( Element of I) -> Element of the carrier of (J . $1) = Bottom (J . $1);
let a be object ; :: thesis: ( ( a in pi ((waybelow x),i9) implies a in waybelow (x . i9) ) & ( a in waybelow (x . i9) implies a in pi ((waybelow x),i9) ) )
consider g being ManySortedSet of I 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 . i9) implies a in pi ((waybelow x),i9) )

assume a in pi ((waybelow x),i9) ; :: thesis: a in waybelow (x . i9)
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 . i9 << x . i9 by A2, WAYBEL_3:33;
hence a in waybelow (x . i9) by A5; :: thesis: verum

end;

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

now :: thesis: for j being Element of I holds (g +* (i,a)) . j is Element of (J . j)

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

per cases ( i9 = j or i9 <> j ) ;

suppose i9 = 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:31; :: thesis: verum

end;

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

then (g +* (i,a)) . j = g . j by FUNCT_7:32
.= 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 :: thesis: for j being Element of I holds f . j << x . j

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

per cases ( i9 = j or i9 <> j ) ;

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

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

end;

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

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

end;

end;

end;

now :: thesis: for j being Element of I st not j in K holds
f . j = Bottom (J . j)

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 <> i9 by TARSKI:def 1;
hence f . j = g . j by FUNCT_7:32
.= 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 . i9 by A6, FUNCT_7:31;
hence a in pi ((waybelow x),i9) by A13, CARD_3:def 6; :: thesis: verum

end;

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

end;

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