deffunc H₁( Real) -> Element of REAL = In ((1 * c₁),REAL);
defpred S₁[ set ] means c₁ in REAL ;
consider f being PartFunc of REAL,REAL such that
A1: ( ( for r being Element of REAL holds
( r in dom f iff S₁[r] ) ) & ( for r being Element of 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 object st y in REAL holds
y in dom f by A1;
then REAL c= dom f ;
then dom f = REAL ;
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

proof

let p be Real; :: thesis: f . p = 1 * p
In ((1 * p),REAL) = 1 * p ;
hence f . p = 1 * p by A1; :: thesis: verum

end;

hence ex r being Real st
for p being Real holds f . p = r * p ; :: thesis: verum