consider F being PartFunc of X,REAL such that
A1: for x being Element of X holds
( x in dom F iff S₁[x] ) and
A2: for x being Element of X st x in dom F holds
F . x = H₁(x) from SEQ_1:sch 3();
take F ; :: thesis: ( dom F = dom f & ( for x being Element of X st x in dom F holds
F . x = ||.(f /. x).|| ) )
thus dom F = dom f by A1, SUBSET_1:8; :: thesis: for x being Element of X st x in dom F holds
F . x = ||.(f /. x).||
let x be Element of X; :: thesis: ( x in dom F implies F . x = ||.(f /. x).|| )
assume x in dom F ; :: thesis: F . x = ||.(f /. x).||
hence F . x = ||.(f /. x).|| by A2; :: thesis: verum