let A be non empty set ; :: thesis: for B being Finite_Subset of 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 Finite_Subset of 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: ( the L_join of L is commutative & the L_join of L is associative & the L_join of L is having_a_unity & Bottom L = the_unity_wrt the L_join of L & the L_join of L is_distributive_wrt the L_join of L & the L_join of L is idempotent ) by Th26, Th34, Th67, Th68;

now

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:40 ;
hence FinJoin B,f [= u by LATTICES:41; :: thesis: verum

end;

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

hence FinJoin B,f [= u by A1, Th47; :: thesis: verum

end;

end;

end;

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