let L be domRing; :: thesis: for p being non-zero Polynomial of L
for B being bag of the carrier of L
for E being Enumeration of Roots p st Roots p = {} holds
B (++) E = {}
let p be non-zero Polynomial of L; :: thesis: for B being bag of the carrier of L
for E being Enumeration of Roots p st Roots p = {} holds
B (++) E = {}
let B be bag of the carrier of L; :: thesis: for E being Enumeration of Roots p st Roots p = {} holds
B (++) E = {}
let E be Enumeration of Roots p; :: thesis: ( Roots p = {} implies B (++) E = {} )
assume A1: Roots p = {} ; :: thesis: B (++) E = {}
A2: len (B (++) E) = len E by Def1;
rng E = Roots p by RLAFFIN3:def 1;
then E = {} by A1;
hence B (++) E = {} by A2; :: thesis: verum