let 0L be lower-bounded Lattice; :: thesis: for B being Finite_Subset of the carrier of 0L
for b being Element of 0L
for f being UnOp of the carrier of 0L holds FinJoin (B \/ {.b.}),f = (FinJoin B,f) "\/" (f . b)
let B be Finite_Subset of the carrier of 0L; :: thesis: for b being Element of 0L
for f being UnOp of the carrier of 0L holds FinJoin (B \/ {.b.}),f = (FinJoin B,f) "\/" (f . b)
let b be Element of 0L; :: thesis: for f being UnOp of the carrier of 0L holds FinJoin (B \/ {.b.}),f = (FinJoin B,f) "\/" (f . b)
let f be UnOp of the carrier of 0L; :: thesis: FinJoin (B \/ {.b.}),f = (FinJoin B,f) "\/" (f . b)
set J = the L_join of 0L;
A1: ( the L_join of 0L is idempotent & the L_join of 0L is commutative & the L_join of 0L is associative & the L_join of 0L is having_a_unity ) by LATTICE2:26, LATTICE2:27, LATTICE2:29, LATTICE2:67;
thus FinJoin (B \/ {.b.}),f = the L_join of 0L $$ (B \/ {.b.}),f by LATTICE2:def 3
.= (the L_join of 0L $$ B,f) "\/" (f . b) by A1, SETWISEO:41
.= (FinJoin B,f) "\/" (f . b) by LATTICE2:def 3 ; :: thesis: verum