let L be non empty antisymmetric complete RelStr ; :: thesis: for F being Function-yielding Function holds
( \// (F,L) = /\\ (F,(L opp)) & /\\ (F,L) = \// (F,(L opp)) )
let F be Function-yielding Function; :: thesis: ( \// (F,L) = /\\ (F,(L opp)) & /\\ (F,L) = \// (F,(L opp)) )

A1: now :: thesis: for x being object st x in dom F holds
(\// (F,L)) . x = (/\\ (F,(L opp))) . x

let x be object ; :: thesis: ( x in dom F implies (\// (F,L)) . x = (/\\ (F,(L opp))) . x )
assume x in dom F ; :: thesis: (\// (F,L)) . x = (/\\ (F,(L opp))) . x
then ( (\// (F,L)) . x = \\/ ((F . x),L) & (/\\ (F,(L opp))) . x = //\ ((F . x),(L opp)) ) by WAYBEL_5:def 1, WAYBEL_5:def 2;
hence (\// (F,L)) . x = (/\\ (F,(L opp))) . x by Th49; :: thesis: verum

end;

( dom (\// (F,L)) = dom F & dom (/\\ (F,(L opp))) = dom F ) by FUNCT_2:def 1;
hence \// (F,L) = /\\ (F,(L opp)) by A1, FUNCT_1:2; :: thesis: /\\ (F,L) = \// (F,(L opp))

A2: now :: thesis: for x being object st x in dom F holds
(/\\ (F,L)) . x = (\// (F,(L opp))) . x

let x be object ; :: thesis: ( x in dom F implies (/\\ (F,L)) . x = (\// (F,(L opp))) . x )
assume x in dom F ; :: thesis: (/\\ (F,L)) . x = (\// (F,(L opp))) . x
then ( (/\\ (F,L)) . x = //\ ((F . x),L) & (\// (F,(L opp))) . x = \\/ ((F . x),(L opp)) ) by WAYBEL_5:def 1, WAYBEL_5:def 2;
hence (/\\ (F,L)) . x = (\// (F,(L opp))) . x by Th49; :: thesis: verum

end;

( dom (/\\ (F,L)) = dom F & dom (\// (F,(L opp))) = dom F ) by FUNCT_2:def 1;
hence /\\ (F,L) = \// (F,(L opp)) by A2, FUNCT_1:2; :: thesis: verum