deffunc H₁( Real) -> Element of REAL = 1 * c₁;
defpred S₁[ set ] means c₁ in REAL ;
consider f being PartFunc of REAL,REAL such that
A1: ( ( for r being Real holds
( r in dom f iff S₁[r] ) ) & ( for r being Real st r in dom f holds
f . r = H₁(r) ) ) from SEQ_1:sch 3();
take f ; :: thesis: f is linear
for y being set st y in REAL holds
y in dom f by A1;
then REAL c= dom f by TARSKI:def 3;
then A2: dom f = REAL by XBOOLE_0:def 10;
hence f is total by PARTFUN1:def 2; :: according to FDIFF_1:def 3 :: thesis: ex r being Real st
for p being Real holds f . p = r * p
for p being Real holds f . p = 1 * p by A1, A2;
hence ex r being Real st
for p being Real holds f . p = r * p ; :: thesis: verum