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 holds
( abs (h /* seq) = (abs h) /* seq & - (h /* seq) = (- h) /* seq )
let h be PartFunc of W,REAL; :: thesis: for seq being sequence of W st rng seq c= dom h holds
( abs (h /* seq) = (abs h) /* seq & - (h /* seq) = (- h) /* seq )
let seq be sequence of W; :: thesis: ( rng seq c= dom h implies ( abs (h /* seq) = (abs h) /* seq & - (h /* seq) = (- h) /* seq ) )
assume A1: rng seq c= dom h ; :: thesis: ( abs (h /* seq) = (abs h) /* seq & - (h /* seq) = (- h) /* seq )
then A2: rng seq c= dom (abs h) by VALUED_1:def 11;
now :: thesis: for n being Element of NAT holds (abs (h /* seq)) . n = ((abs h) /* seq) . n
let n be Element of NAT ; :: thesis: (abs (h /* seq)) . n = ((abs h) /* seq) . n
thus (abs (h /* seq)) . n = |.((h /* seq) . n).| by SEQ_1:12
.= |.(h . (seq . n)).| by A1, FUNCT_2:108
.= (abs h) . (seq . n) by VALUED_1:18
.= ((abs h) /* seq) . n by A2, FUNCT_2:108 ; :: thesis: verum
end;
hence abs (h /* seq) = (abs h) /* seq by FUNCT_2:63; :: thesis: - (h /* seq) = (- h) /* seq
thus - (h /* seq) = (- 1) (#) (h /* seq)
.= ((- 1) (#) h) /* seq by A1, Th9
.= (- h) /* seq ; :: thesis: verum