let L be Lattice; :: thesis: for u being Element of L
for A being non empty set
for B being Element of Fin A
for f being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds
f . x [= u ) holds
FinJoin (B,f) [= u
let u be Element of L; :: thesis: for A being non empty set
for B being Element of Fin A
for f being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds
f . x [= u ) holds
FinJoin (B,f) [= u
let A be non empty set ; :: thesis: for B being Element of Fin A
for f being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds
f . x [= u ) holds
FinJoin (B,f) [= u
let B be Element of Fin A; :: thesis: for f being Function of A, the carrier of L st B <> {} & ( for x being Element of A st x in B holds
f . x [= u ) holds
FinJoin (B,f) [= u
let f be Function of A, the carrier of L; :: thesis: ( B <> {} & ( for x being Element of A st x in B holds
f . x [= u ) implies FinJoin (B,f) [= u )
assume that
A1: B <> {} and
A2: for x being Element of A st x in B holds
f . x [= u ; :: thesis: FinJoin (B,f) [= u
set J = the L_join of L;

A3: now :: thesis: for x being Element of A st x in B holds
( the L_join of L [:] (f,u)) . x = u

let x be Element of A; :: thesis: ( x in B implies ( the L_join of L [:] (f,u)) . x = u )
assume x in B ; :: thesis: ( the L_join of L [:] (f,u)) . x = u
then A4: f . x [= u by A2;
thus ( the L_join of L [:] (f,u)) . x = (f . x) "\/" u by FUNCOP_1:48
.= u by A4 ; :: thesis: verum

end;

(FinJoin (B,f)) "\/" u = the L_join of L $$ (B,( the L_join of L [:] (f,u))) by A1, Th20, SETWISEO:28
.= u by A1, A3, SETWISEO:24 ;
hence FinJoin (B,f) [= u ; :: thesis: verum