let R be Ring; :: thesis: for V being strict LeftMod of strict
for A being Subset of st 0. R <> 1. R & A = the carrier of V holds
Lin A = V
let V be strict LeftMod of strict ; :: thesis: for A being Subset of st 0. R <> 1. R & A = the carrier of V holds
Lin A = V
let A be Subset of ; :: thesis: ( 0. R <> 1. R & A = the carrier of V implies Lin A = V )
assume that
A1: 0. R <> 1. R and
A2: A = the carrier of V ; :: thesis: Lin A = V
A = the carrier of ((Omega). V) by A2;
hence Lin A = V by A1, Th15; :: thesis: verum