let F, G be ext-real-membered set ; :: thesis: for r being real number st r <> 0 holds
r ** (F \+\ G) = (r ** F) \+\ (r ** G)
let r be real number ; :: 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 Th88
.= ((r ** F) \ (r ** G)) \/ (r ** (G \ F)) by A1, Th197
.= (r ** F) \+\ (r ** G) by A1, Th197 ; :: thesis: verum