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 Def35;
hence A2: dom (</> (</> f)) = dom f by Def35; :: 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 Def35
.= ((f . x) ") " by A1, A2, A3, Def35
.= f . x ;
:: thesis: verum