let I be non empty set ; :: thesis:
let J be RelStr-yielding non-Empty reflexive-yielding ManySortedSet of I; :: thesis:
assume A1: for i being Element of I holds J . i is complete continuous LATTICE ; :: thesis:
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:

let x be Element of (product J); :: thesis:
reconsider x9 = x as Element of pJ9 ;
not waybelow x9 is empty ;
hence not waybelow x is empty ; :: thesis:
waybelow x9 is directed ;
hence waybelow x is directed ; :: thesis:

end;

pJ9 is up-complete ;
hence product J is up-complete ; :: thesis:
let x be Element of (product J); :: according to WAYBEL_3:def 5 :: thesis:
set swx = sup (waybelow x);

thus dom x = I by WAYBEL_3:27; :: thesis:
thus dom (sup (waybelow x)) = I by WAYBEL_3:27; :: thesis:
let i be object ; :: thesis:
assume i in I ; :: thesis:
then reconsider i9 = i as Element of I ;

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:
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:

assume a in pi ((waybelow x),i9) ; :: thesis:
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:

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:

let j be Element of I; :: thesis:

suppose i9 = j ; :: thesis:

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

end;

suppose i9 <> j ; :: thesis:

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:

end;

end;

end;

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

A9: now :: thesis:

let j be Element of I; :: thesis:

suppose A10: i9 = j ; :: thesis:

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

end;

suppose A11: i9 <> j ; :: thesis:

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:

end;

end;

end;

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

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:

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:

end;

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