let L be Field; :: thesis: for m being Element of NAT st m > 0 holds
for p, q being Polynomial of L holds (emb (2 * m),L) * ((1. L,(2 * m)) * (mConv (p *' q),(2 * m))) = (emb (2 * m),L) * (mConv (p *' q),(2 * m))
let m be Element of NAT ; :: thesis: ( m > 0 implies for p, q being Polynomial of L holds (emb (2 * m),L) * ((1. L,(2 * m)) * (mConv (p *' q),(2 * m))) = (emb (2 * m),L) * (mConv (p *' q),(2 * m)) )
assume A1: m > 0 ; :: thesis: for p, q being Polynomial of L holds (emb (2 * m),L) * ((1. L,(2 * m)) * (mConv (p *' q),(2 * m))) = (emb (2 * m),L) * (mConv (p *' q),(2 * m))
let p, q be Polynomial of L; :: thesis: (emb (2 * m),L) * ((1. L,(2 * m)) * (mConv (p *' q),(2 * m))) = (emb (2 * m),L) * (mConv (p *' q),(2 * m))
2 * m > 2 * 0 by A1, XREAL_1:70;
hence (emb (2 * m),L) * ((1. L,(2 * m)) * (mConv (p *' q),(2 * m))) = (emb (2 * m),L) * (mConv (p *' q),(2 * m)) by Th35; :: thesis: verum