let A be non empty set ; :: thesis: for B being Element of Fin A
for L being 0_Lattice
for f being Function of A, the carrier of L
for u being Element of L st ( 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 L being 0_Lattice
for f being Function of A, the carrier of L
for u being Element of L st ( for x being Element of A st x in B holds
f . x [= u ) holds
FinJoin (B,f) [= u
let L be 0_Lattice; :: thesis: for f being Function of A, the carrier of L
for u being Element of L st ( 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: for u being Element of L st ( 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 x being Element of A st x in B holds
f . x [= u ) implies FinJoin (B,f) [= u )
assume A1: 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;
A2: Bottom L = the_unity_wrt the L_join of L by Th18;

now :: thesis: FinJoin (B,f) [= u

per cases ( B = {} or B <> {} ) ;

suppose B = {} ; :: thesis: FinJoin (B,f) [= u

then FinJoin (B,f) = the L_join of L $$ (({}. A),f)
.= Bottom L by A2, SETWISEO:31 ;
hence FinJoin (B,f) [= u ; :: thesis: verum

end;

suppose B <> {} ; :: thesis: FinJoin (B,f) [= u

hence FinJoin (B,f) [= u by A1, Th32; :: thesis: verum

end;

end;

end;

hence FinJoin (B,f) [= u ; :: thesis: verum