let X, X1 be set ; :: thesis: for Y, Y1 being complex-functions-membered set
for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1 st f1 = abs f holds
abs f1 = abs f
let Y, Y1 be complex-functions-membered set ; :: thesis: for f being PartFunc of X,Y
for f1 being PartFunc of X1,Y1 st f1 = abs f holds
abs f1 = abs f
let f be PartFunc of X,Y; :: thesis: for f1 being PartFunc of X1,Y1 st f1 = abs f holds
abs f1 = abs f
let f1 be PartFunc of X1,Y1; :: thesis: ( f1 = abs f implies abs f1 = abs f )
assume A1: f1 = abs f ; :: thesis: abs f1 = abs f
hence A2: dom (abs f1) = dom (abs f) by Def35; :: according to FUNCT_1:def 17 :: thesis: for b₁ being set holds
( not b₁ in dom (abs f1) or (abs f1) . b₁ = (abs f) . b₁ )
let x be set ; :: thesis: ( not x in dom (abs f1) or (abs f1) . x = (abs f) . x )
assume A3: x in dom (abs f1) ; :: thesis: (abs f1) . x = (abs f) . x
hence (abs f1) . x = abs (f1 . x) by Def35
.= abs (abs (f . x)) by A1, A2, A3, Def35
.= (abs f) . x by A2, A3, Def35 ;
:: thesis: verum