let X be set ; :: thesis: for Y being complex-functions-membered set
for f being PartFunc of X,Y holds <-> (<-> f) = f
let Y be complex-functions-membered set ; :: thesis: for f being PartFunc of X,Y holds <-> (<-> f) = f
let f be PartFunc of X,Y; :: thesis: <-> (<-> f) = f
set f1 = <-> f;
A1: dom (<-> f) = dom f by Def33;
hence A2: dom (<-> (<-> f)) = dom f by Def33; :: according to FUNCT_1:def 11 :: thesis: for b₁ being object holds
( not b₁ in dom (<-> (<-> f)) or (<-> (<-> f)) . b₁ = f . b₁ )
let x be object ; :: thesis: ( not x in dom (<-> (<-> f)) or (<-> (<-> f)) . x = f . x )
assume A3: x in dom (<-> (<-> f)) ; :: thesis: (<-> (<-> f)) . x = f . x
hence (<-> (<-> f)) . x = - ((<-> f) . x) by Def33
.= - (- (f . x)) by A1, A2, A3, Def33
.= f . x ;
:: thesis: verum