let f be complex-valued Function; :: thesis: (f ^) ^ = f | (dom (f ^))

A1: dom ((f ^) ^) = dom (f | (dom (f ^))) by Th6;

A1: dom ((f ^) ^) = dom (f | (dom (f ^))) by Th6;

now :: thesis: for c being object st c in dom ((f ^) ^) holds

((f ^) ^) . c = (f | (dom (f ^))) . c

hence
(f ^) ^ = f | (dom (f ^))
by A1, FUNCT_1:2; :: thesis: verum((f ^) ^) . c = (f | (dom (f ^))) . c

let c be object ; :: thesis: ( c in dom ((f ^) ^) implies ((f ^) ^) . c = (f | (dom (f ^))) . c )

assume A2: c in dom ((f ^) ^) ; :: thesis: ((f ^) ^) . c = (f | (dom (f ^))) . c

then c in (dom f) /\ (dom (f ^)) by A1, RELAT_1:61;

then A3: c in dom (f ^) by XBOOLE_0:def 4;

thus ((f ^) ^) . c = ((f ^) . c) " by A2, Def2

.= ((f . c) ") " by A3, Def2

.= (f | (dom (f ^))) . c by A1, A2, FUNCT_1:47 ; :: thesis: verum

end;assume A2: c in dom ((f ^) ^) ; :: thesis: ((f ^) ^) . c = (f | (dom (f ^))) . c

then c in (dom f) /\ (dom (f ^)) by A1, RELAT_1:61;

then A3: c in dom (f ^) by XBOOLE_0:def 4;

thus ((f ^) ^) . c = ((f ^) . c) " by A2, Def2

.= ((f . c) ") " by A3, Def2

.= (f | (dom (f ^))) . c by A1, A2, FUNCT_1:47 ; :: thesis: verum