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_{1} being object holds

( not b_{1} in dom (<-> (<-> f)) or (<-> (<-> f)) . b_{1} = f . b_{1} )

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

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

( not 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