let F be real-valued FinSequence; :: thesis: ( (<*> REAL ) - F = <*> REAL & F - (<*> REAL ) = <*> REAL )
F is FinSequence of REAL by Lm4;
hence ( (<*> REAL ) - F = <*> REAL & F - (<*> REAL ) = <*> REAL ) by FINSEQ_2:87; :: thesis: verum