let 0L be lower-bounded Lattice; :: thesis: for B being Element of Fin 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 Element of Fin 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;

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 SETWISEO:32

.= (FinJoin (B,f)) "\/" (f . b) by LATTICE2:def 3 ; :: thesis: verum

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 Fin 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;

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 SETWISEO:32

.= (FinJoin (B,f)) "\/" (f . b) by LATTICE2:def 3 ; :: thesis: verum