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
h /* seq is non-zero
let h be PartFunc of W,REAL; :: thesis: for seq being sequence of W st rng seq c= dom (h ^) holds
h /* seq is non-zero
let seq be sequence of W; :: 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
then A2: ( (dom h) \ (h " {0}) c= dom h & rng seq c= (dom h) \ (h " {0}) ) by RFUNCT_1:def 2, XBOOLE_1:36;
now :: thesis: for n being Nat holds not (h /* seq) . n = 0
given n being Nat such that A3: (h /* seq) . n = 0 ; :: thesis: contradiction
A4: n in NAT by ORDINAL1:def 12;
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 2;
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 7;
h . (seq . n) = 0 by A2, A3, FUNCT_2:108, XBOOLE_1:1, A4;
hence contradiction by A5, TARSKI:def 1; :: thesis: verum
end;
hence h /* seq is non-zero by SEQ_1:5; :: thesis: verum