let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; :: thesis: doubleLoopStr(# the carrier of (), the addF of (), the multF of (), the OneF of (), the ZeroF of () #) = Polynom-Ring L
A1: ex A being non empty Subset of () st
( A = the carrier of () & Polynom-Algebra L = GenAlg A ) by Def6;
then A2: the carrier of () = the carrier of () by ;
A3: the carrier of () c= the carrier of () by ;
A4: for x being Element of ()
for y being Element of () holds the addF of () . (x,y) = the addF of () . (x,y)
proof
let x be Element of (); :: thesis: for y being Element of () holds the addF of () . (x,y) = the addF of () . (x,y)
let y be Element of (); :: thesis: the addF of () . (x,y) = the addF of () . (x,y)
reconsider y1 = y as Element of () by ;
reconsider y9 = y1 as Element of () by ;
reconsider x9 = x as Element of () by A3;
reconsider p = x as AlgSequence of L by ;
reconsider x1 = x as Element of () by ;
reconsider q = y as AlgSequence of L by POLYNOM3:def 10;
thus the addF of () . (x,y) = x + y1
.= x9 + y9 by
.= p + q by Def2
.= x1 + y by POLYNOM3:def 10
.= the addF of () . (x,y) ; :: thesis: verum
end;
now :: thesis: for x being Element of ()
for y being Element of () holds the multF of () . (x,y) = the multF of () . (x,y)
let x be Element of (); :: thesis: for y being Element of () holds the multF of () . (x,y) = the multF of () . (x,y)
let y be Element of (); :: thesis: the multF of () . (x,y) = the multF of () . (x,y)
reconsider y1 = y as Element of () by ;
reconsider y9 = y1 as Element of () by ;
reconsider x9 = x as Element of () by A3;
reconsider p = x as AlgSequence of L by ;
reconsider x1 = x as Element of () by ;
reconsider q = y as AlgSequence of L by POLYNOM3:def 10;
thus the multF of () . (x,y) = x * y1
.= x9 * y9 by
.= p *' q by Def2
.= x1 * y by POLYNOM3:def 10
.= the multF of () . (x,y) ; :: thesis: verum
end;
then A5: the multF of () = the multF of () by ;
A6: 1. () = 1. () by
.= 1_. L by Def2
.= 1. () by POLYNOM3:def 10 ;
0. () = 0. () by
.= 0_. L by Def2
.= 0. () by POLYNOM3:def 10 ;
hence doubleLoopStr(# the carrier of (), the addF of (), the multF of (), the OneF of (), the ZeroF of () #) = Polynom-Ring L by ; :: thesis: verum