let F, G be ext-real-membered set ; :: thesis: for r being Real st r <> 0 holds
r ** (F \+\ G) = (r ** F) \+\ (r ** G)
let r be Real; :: thesis: ( r <> 0 implies r ** (F \+\ G) = (r ** F) \+\ (r ** G) )
assume A1: r <> 0 ; :: thesis: r ** (F \+\ G) = (r ** F) \+\ (r ** G)
thus r ** (F \+\ G) = (r ** (F \ G)) \/ (r ** (G \ F)) by Th82
.= ((r ** F) \ (r ** G)) \/ (r ** (G \ F)) by A1, Th191
.= (r ** F) \+\ (r ** G) by A1, Th191 ; :: thesis: verum