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 ;
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 ; :: 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 ;
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 ; :: thesis: verum