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)) )

hence \// (F,L) = /\\ (F,(L opp)) by A1, FUNCT_1:2; :: thesis: /\\ (F,L) = \// (F,(L opp))

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

( \// (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

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

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

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

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