let X be set ; :: thesis: for seq being Real_Sequence
for h being PartFunc of REAL ,REAL st rng seq c= dom (h | X) holds
abs ((h | X) /* seq) = ((abs h) | X) /* seq
let seq be Real_Sequence; :: thesis: for h being PartFunc of REAL ,REAL st rng seq c= dom (h | X) holds
abs ((h | X) /* seq) = ((abs h) | X) /* seq
let h be PartFunc of REAL ,REAL ; :: thesis: ( rng seq c= dom (h | X) implies abs ((h | X) /* seq) = ((abs h) | X) /* seq )
assume A1: rng seq c= dom (h | X) ; :: thesis: abs ((h | X) /* seq) = ((abs h) | X) /* seq
A2: dom (h | X) = (dom h) /\ X by RELAT_1:90
.= (dom (abs h)) /\ X by VALUED_1:def 11
.= dom ((abs h) | X) by RELAT_1:90 ;

now

let n be Element of NAT ; :: thesis: (abs ((h | X) /* seq)) . n = (((abs h) | X) /* seq) . n
A3: seq . n in rng seq by VALUED_0:28;
then seq . n in dom (h | X) by A1;
then seq . n in (dom h) /\ X by RELAT_1:90;
then A4: seq . n in X by XBOOLE_0:def 4;
thus (abs ((h | X) /* seq)) . n = abs (((h | X) /* seq) . n) by SEQ_1:16
.= abs ((h | X) . (seq . n)) by A1, FUNCT_2:185
.= abs (h . (seq . n)) by A1, A3, FUNCT_1:70
.= (abs h) . (seq . n) by VALUED_1:18
.= ((abs h) | X) . (seq . n) by A4, FUNCT_1:72
.= (((abs h) | X) /* seq) . n by A1, A2, FUNCT_2:185 ; :: thesis: verum

end;

hence abs ((h | X) /* seq) = ((abs h) | X) /* seq by FUNCT_2:113; :: thesis: verum