set f = <*455,780,1092,5460,420*>;
set s = 4;
set g = <*455,780,1092,5460,420*> | 4;
A1: <*455,780,1092,5460,420*> = <*455,780,1092,5460*> ^ <*420*> by FINSEQ_4:75;
((<*455,780,1092,5460,420*> | 4) (#) (<*455,780,1092,5460,420*> | 4)) " = ((<*455,780,1092,5460,420*> | 4) ") (#) ((<*455,780,1092,5460,420*> | 4) ") by Th50;
then A2: (((<*455,780,1092,5460,420*> | 4) (#) (<*455,780,1092,5460,420*> | 4)) (#) (<*455,780,1092,5460,420*> | 4)) " = (((<*455,780,1092,5460,420*> | 4) ") (#) ((<*455,780,1092,5460,420*> | 4) ")) (#) ((<*455,780,1092,5460,420*> | 4) ") by Th50;
A3: (<*455,780,1092,5460,420*> | 4) " = <*(455 "),(780 "),(1092 "),(5460 ")*> by A1, Th15;
A4: <*(455 "),(780 "),(1092 "),(5460 ")*> (#) <*(455 "),(780 "),(1092 "),(5460 ")*> = <*((455 ") * (455 ")),((780 ") * (780 ")),((1092 ") * (1092 ")),((5460 ") * (5460 "))*> by FINSEQ_9:47;
A5: <*((455 ") * (455 ")),((780 ") * (780 ")),((1092 ") * (1092 ")),((5460 ") * (5460 "))*> (#) <*(455 "),(780 "),(1092 "),(5460 ")*> = <*(((455 ") * (455 ")) * (455 ")),(((780 ") * (780 ")) * (780 ")),(((1092 ") * (1092 ")) * (1092 ")),(((5460 ") * (5460 ")) * (5460 "))*> by FINSEQ_9:47;
(<*455,780,1092,5460,420*> . (4 + 1)) |^ 3 = ((<*455,780,1092,5460,420*> . (4 + 1)) * (<*455,780,1092,5460,420*> . (4 + 1))) * (<*455,780,1092,5460,420*> . (4 + 1)) by POLYEQ_5:2;
hence 1 / ((<*455,780,1092,5460,420*> . (4 + 1)) |^ 3) = (((((455 ") * (455 ")) * (455 ")) + (((780 ") * (780 ")) * (780 "))) + (((1092 ") * (1092 ")) * (1092 "))) + (((5460 ") * (5460 ")) * (5460 "))
.= Sum ((((<*455,780,1092,5460,420*> | 4) (#) (<*455,780,1092,5460,420*> | 4)) (#) (<*455,780,1092,5460,420*> | 4)) ") by A2, A3, A4, A5, Th20 ;
:: according to NUMBER17:def 17 :: thesis: verum