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: ( dom (\// F,L) = dom F & dom (/\\ F,(L opp )) = dom F ) by FUNCT_2:def 1;

now

let x be set ; :: 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;

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

now

let x be set ; :: 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;

hence /\\ F,L = \// F,(L opp ) by A2, FUNCT_1:9; :: thesis: verum