A1: 2 |^ 4 = ((2 * 2) * 2) * 2 by POLYEQ_5:3;
A2: 3 |^ 4 = ((3 * 3) * 3) * 3 by POLYEQ_5:3;
A3: 4 |^ 4 = ((4 * 4) * 4) * 4 by POLYEQ_5:3;
A4: 5 |^ 4 = ((5 * 5) * 5) * 5 by POLYEQ_5:3;
thus 2 = (1 |^ 4) + (1 |^ 4) ; :: thesis: ( 17 = (1 |^ 4) + (2 |^ 4) & 97 = (2 |^ 4) + (3 |^ 4) & 257 = (1 |^ 4) + (4 |^ 4) & 641 = (2 |^ 4) + (5 |^ 4) )
thus 17 = (1 |^ 4) + (2 |^ 4) by A1; :: thesis: ( 97 = (2 |^ 4) + (3 |^ 4) & 257 = (1 |^ 4) + (4 |^ 4) & 641 = (2 |^ 4) + (5 |^ 4) )
thus 97 = (2 |^ 4) + (3 |^ 4) by A1, A2; :: thesis: ( 257 = (1 |^ 4) + (4 |^ 4) & 641 = (2 |^ 4) + (5 |^ 4) )
thus 257 = (1 |^ 4) + (4 |^ 4) by A3; :: thesis: 641 = (2 |^ 4) + (5 |^ 4)
thus 641 = (2 |^ 4) + (5 |^ 4) by A1, A4; :: thesis: verum