let R be domRing; :: thesis: for V being strict RightMod of R
for A being Subset of V st 0. R <> 1_ R & A = the carrier of V holds
Lin A = V
let V be strict RightMod of R; :: thesis: for A being Subset of V st 0. R <> 1_ R & A = the carrier of V holds
Lin A = V
let A be Subset of V; :: thesis: ( 0. R <> 1_ R & A = the carrier of V implies Lin A = V )
assume A1: 0. R <> 1_ R ; :: thesis: ( not A = the carrier of V or Lin A = V )
assume A2: A = the carrier of V ; :: thesis: Lin A = V
(Omega). V = V ;
hence Lin A = V by A1, A2, Th71; :: thesis: verum