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 FinJoin (B,f) [= u holds
for x being Element of A st x in B holds
f . x [= 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 FinJoin (B,f) [= u holds
for x being Element of A st x in B holds
f . x [= 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 FinJoin (B,f) [= u holds
for x being Element of A st x in B holds
f . x [= u
let B be Element of Fin A; :: thesis: for f being Function of A, the carrier of L st FinJoin (B,f) [= u holds
for x being Element of A st x in B holds
f . x [= u
let f be Function of A, the carrier of L; :: thesis: ( FinJoin (B,f) [= u implies for x being Element of A st x in B holds
f . x [= u )
assume A1: FinJoin (B,f) [= u ; :: thesis: for x being Element of A st x in B holds
f . x [= u
let x be Element of A; :: thesis: ( x in B implies f . x [= u )
assume x in B ; :: thesis: f . x [= u
then f . x [= FinJoin (B,f) by Th28;
hence f . x [= u by A1, LATTICES:7; :: thesis: verum