let A be set ; :: thesis: for D being non empty set
for o, o9 being BinOp of D st o absorbs o9 holds
o,D .: A absorbs o9,D .: A
let D be non empty set ; :: thesis: for o, o9 being BinOp of D st o absorbs o9 holds
o,D .: A absorbs o9,D .: A
let o, o9 be BinOp of D; :: thesis: ( o absorbs o9 implies o,D .: A absorbs o9,D .: A )
assume A1: for a, b being Element of D holds o . a,(o9 . a,b) = a ; :: according to LATTICE2:def 1 :: thesis: o,D .: A absorbs o9,D .: A
let f, g be Element of Funcs A,D; :: according to LATTICE2:def 1 :: thesis: (o,D .: A) . f,((o9,D .: A) . f,g) = f
A2: dom (o .: f,(o9 .: f,g)) = A by FUNCT_2:def 1;
A3: dom (o9 .: f,g) = A by FUNCT_2:def 1;

A4: now

let x be set ; :: thesis: ( x in A implies f . x = (o .: f,(o9 .: f,g)) . x )
assume A5: x in A ; :: thesis: f . x = (o .: f,(o9 .: f,g)) . x
then reconsider a = f . x, b = g . x as Element of D by FUNCT_2:7;
( (o .: f,(o9 .: f,g)) . x = o . a,((o9 .: f,g) . x) & (o9 .: f,g) . x = o9 . a,b ) by A3, A2, A5, FUNCOP_1:28;
hence f . x = (o .: f,(o9 .: f,g)) . x by A1; :: thesis: verum

end;

A6: dom f = A by FUNCT_2:def 1;
( (o9,D .: A) . f,g = o9 .: f,g & (o,D .: A) . f,(o9 .: f,g) = o .: f,(o9 .: f,g) ) by Def2;
hence (o,D .: A) . f,((o9,D .: A) . f,g) = f by A6, A2, A4, FUNCT_1:9; :: thesis: verum