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:5;
( (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:22;
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:2; :: thesis: verum