let seq be Real_Sequence; :: thesis: for h being PartFunc of REAL , REAL st rng seq c= dom (h ^ ) holds
h /* seq is non-zero
let h be PartFunc of REAL , REAL ; :: thesis: ( rng seq c= dom (h ^ ) implies h /* seq is non-zero )
assume A1: rng seq c= dom (h ^ ) ; :: thesis: h /* seq is non-zero
A2: (dom h) \ (h " {0 }) c= dom h by XBOOLE_1:36;
A3: rng seq c= (dom h) \ (h " {0 }) by A1, RFUNCT_1:def 8;

now

given n being Element of NAT such that A4: (h /* seq) . n = 0 ; :: thesis: contradiction
seq . n in rng seq by VALUED_0:28;
then seq . n in dom (h ^ ) by A1;
then seq . n in (dom h) \ (h " {0 }) by RFUNCT_1:def 8;
then ( seq . n in dom h & not seq . n in h " {0 } ) by XBOOLE_0:def 5;
then A5: not h . (seq . n) in {0 } by FUNCT_1:def 13;
h . (seq . n) = 0 by A2, A3, A4, FUNCT_2:185, XBOOLE_1:1;
hence contradiction by A5, TARSKI:def 1; :: thesis: verum

end;

hence h /* seq is non-zero by SEQ_1:7; :: thesis: verum