let X be set ; :: thesis: for W being non empty set

for h being PartFunc of W,REAL

for seq being sequence of W st rng seq c= dom (h | X) holds

abs ((h | X) /* seq) = ((abs h) | X) /* seq

let W be non empty set ; :: thesis: for h being PartFunc of W,REAL

for seq being sequence of W st rng seq c= dom (h | X) holds

abs ((h | X) /* seq) = ((abs h) | X) /* seq

let h be PartFunc of W,REAL; :: thesis: for seq being sequence of W st rng seq c= dom (h | X) holds

abs ((h | X) /* seq) = ((abs h) | X) /* seq

let seq be sequence of W; :: 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:61

.= (dom (abs h)) /\ X by VALUED_1:def 11

.= dom ((abs h) | X) by RELAT_1:61 ;

for h being PartFunc of W,REAL

for seq being sequence of W st rng seq c= dom (h | X) holds

abs ((h | X) /* seq) = ((abs h) | X) /* seq

let W be non empty set ; :: thesis: for h being PartFunc of W,REAL

for seq being sequence of W st rng seq c= dom (h | X) holds

abs ((h | X) /* seq) = ((abs h) | X) /* seq

let h be PartFunc of W,REAL; :: thesis: for seq being sequence of W st rng seq c= dom (h | X) holds

abs ((h | X) /* seq) = ((abs h) | X) /* seq

let seq be sequence of W; :: 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:61

.= (dom (abs h)) /\ X by VALUED_1:def 11

.= dom ((abs h) | X) by RELAT_1:61 ;

now :: thesis: for n being Element of NAT holds (abs ((h | X) /* seq)) . n = (((abs h) | X) /* seq) . n

hence
abs ((h | X) /* seq) = ((abs h) | X) /* seq
by FUNCT_2:63; :: thesis: verumlet 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:61;

then A4: seq . n in X by XBOOLE_0:def 4;

thus (abs ((h | X) /* seq)) . n = |.(((h | X) /* seq) . n).| by SEQ_1:12

.= |.((h | X) . (seq . n)).| by A1, FUNCT_2:108

.= |.(h . (seq . n)).| by A1, A3, FUNCT_1:47

.= (abs h) . (seq . n) by VALUED_1:18

.= ((abs h) | X) . (seq . n) by A4, FUNCT_1:49

.= (((abs h) | X) /* seq) . n by A1, A2, FUNCT_2:108 ; :: thesis: verum

end;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:61;

then A4: seq . n in X by XBOOLE_0:def 4;

thus (abs ((h | X) /* seq)) . n = |.(((h | X) /* seq) . n).| by SEQ_1:12

.= |.((h | X) . (seq . n)).| by A1, FUNCT_2:108

.= |.(h . (seq . n)).| by A1, A3, FUNCT_1:47

.= (abs h) . (seq . n) by VALUED_1:18

.= ((abs h) | X) . (seq . n) by A4, FUNCT_1:49

.= (((abs h) | X) /* seq) . n by A1, A2, FUNCT_2:108 ; :: thesis: verum