let R be domRing; :: thesis: for n being non empty Ordinal
for f, g being Polynomial of n,R holds Zero_ {(f *' g)} = (Zero_ {f}) \/ (Zero_ {g})
let n be non empty Ordinal; :: thesis: for f, g being Polynomial of n,R holds Zero_ {(f *' g)} = (Zero_ {f}) \/ (Zero_ {g})
let f, g be Polynomial of n,R; :: thesis: Zero_ {(f *' g)} = (Zero_ {f}) \/ (Zero_ {g})
A1: for o being object st o in Zero_ {(f *' g)} holds
o in (Zero_ {f}) \/ (Zero_ {g})

proof

let o be object ; :: thesis: ( o in Zero_ {(f *' g)} implies o in (Zero_ {f}) \/ (Zero_ {g}) )
assume o in Zero_ {(f *' g)} ; :: thesis: o in (Zero_ {f}) \/ (Zero_ {g})
then o in Zero_ (f *' g) by Th15;
then consider x being Function of n,R such that
A4: ( x = o & eval ((f *' g),x) = 0. R ) ;
reconsider x1 = eval (f,x) as Element of R ;
reconsider x2 = eval (g,x) as Element of R ;
A5: 0. R = x1 * x2 by A4, POLYNOM2:25;
( eval (f,x) = 0. R or eval (g,x) = 0. R ) by A5, VECTSP_2:def 1;
then ( o in Zero_ f or o in Zero_ g ) by A4;
then ( o in Zero_ {f} or o in Zero_ {g} ) by Th15;
hence o in (Zero_ {f}) \/ (Zero_ {g}) by XBOOLE_0:def 3; :: thesis: verum

end;

for o being object st o in (Zero_ {f}) \/ (Zero_ {g}) holds
o in Zero_ {(f *' g)}

proof

let o be object ; :: thesis: ( o in (Zero_ {f}) \/ (Zero_ {g}) implies o in Zero_ {(f *' g)} )
assume o in (Zero_ {f}) \/ (Zero_ {g}) ; :: thesis: o in Zero_ {(f *' g)}
then ( o in Zero_ {f} or o in Zero_ {g} ) by XBOOLE_0:def 3;

per cases then ( o in Zero_ f or o in Zero_ g ) by Th15;

suppose o in Zero_ f ; :: thesis: o in Zero_ {(f *' g)}

then consider x being Function of n,R such that
A10: ( o = x & eval (f,x) = 0. R ) ;
reconsider x1 = eval (g,x) as Element of R ;
eval ((f *' g),x) = (0. R) * x1 by A10, POLYNOM2:25
.= 0. R ;
then o in Zero_ (f *' g) by A10;
hence o in Zero_ {(f *' g)} by Th15; :: thesis: verum

end;

suppose o in Zero_ g ; :: thesis: o in Zero_ {(f *' g)}

then consider x being Function of n,R such that
A13: ( o = x & eval (g,x) = 0. R ) ;
reconsider x1 = eval (f,x) as Element of R ;
eval ((f *' g),x) = x1 * (0. R) by A13, POLYNOM2:25
.= 0. R ;
then o in Zero_ (f *' g) by A13;
hence o in Zero_ {(f *' g)} by Th15; :: thesis: verum

end;

end;

end;

hence Zero_ {(f *' g)} = (Zero_ {f}) \/ (Zero_ {g}) by A1, TARSKI_0:2; :: thesis: verum