set f = <*12,15,20,10*>;
set s = 3;
set g = <*12,15,20,10*> | 3;
((<*12,15,20,10*> | 3) (#) (<*12,15,20,10*> | 3)) " = ((<*12,15,20,10*> | 3) ") (#) ((<*12,15,20,10*> | 3) ") by Th50;
then A1: (((<*12,15,20,10*> | 3) (#) (<*12,15,20,10*> | 3)) (#) (<*12,15,20,10*> | 3)) " = (((<*12,15,20,10*> | 3) ") (#) ((<*12,15,20,10*> | 3) ")) (#) ((<*12,15,20,10*> | 3) ") by Th50;
A2: (<*12,15,20,10*> | 3) " = <*(12 "),(15 "),(20 ")*> by NUMBER15:65;
A3: <*(12 "),(15 "),(20 ")*> (#) <*(12 "),(15 "),(20 ")*> = <*((12 ") * (12 ")),((15 ") * (15 ")),((20 ") * (20 "))*> by FINSEQ_9:46;
A4: <*((12 ") * (12 ")),((15 ") * (15 ")),((20 ") * (20 "))*> (#) <*(12 "),(15 "),(20 ")*> = <*(((12 ") * (12 ")) * (12 ")),(((15 ") * (15 ")) * (15 ")),(((20 ") * (20 ")) * (20 "))*> by FINSEQ_9:46;
(<*12,15,20,10*> . (3 + 1)) |^ 3 = ((<*12,15,20,10*> . (3 + 1)) * (<*12,15,20,10*> . (3 + 1))) * (<*12,15,20,10*> . (3 + 1)) by POLYEQ_5:2;
hence 1 / ((<*12,15,20,10*> . (3 + 1)) |^ 3) = ((((12 ") * (12 ")) * (12 ")) + (((15 ") * (15 ")) * (15 "))) + (((20 ") * (20 ")) * (20 "))
.= Sum ((((<*12,15,20,10*> | 3) (#) (<*12,15,20,10*> | 3)) (#) (<*12,15,20,10*> | 3)) ") by A1, A2, A3, A4, RVSUM_2:35 ;
:: according to NUMBER17:def 17 :: thesis: verum