set E = { f where f is Function of R,R : f is derivation } ;
for o being object st o in { f where f is Function of R,R : f is derivation } holds
o in Funcs (([#] R),([#] R))

proof

let o be object ; :: thesis: ( o in { f where f is Function of R,R : f is derivation } implies o in Funcs (([#] R),([#] R)) )
assume o in { f where f is Function of R,R : f is derivation } ; :: thesis: o in Funcs (([#] R),([#] R))
then consider f being Function of R,R such that
A2: ( f = o & f is derivation ) ;
A3: dom f = [#] R by FUNCT_2:def 1;
rng f c= [#] R ;
hence o in Funcs (([#] R),([#] R)) by A2, A3, FUNCT_2:def 2; :: thesis: verum

end;

hence { f where f is Function of R,R : f is derivation } is Subset of (Funcs (([#] R),([#] R))) by TARSKI:def 3; :: thesis: verum