let p be Prime; :: thesis: for n being Nat ex x1, x2, x3, x4 being Nat st p |^ n = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2)
let n be Nat; :: thesis: ex x1, x2, x3, x4 being Nat st p |^ n = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2)
defpred S₁[ Nat] means ex x1, x2, x3, x4 being Nat st p |^ $1 = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2);
A1: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then consider x1, x2, x3, x4 being Nat such that
A3: p |^ n = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2) ;
consider y1, y2, y3, y4 being Nat such that
A4: p = (((y1 ^2) + (y2 ^2)) + (y3 ^2)) + (y4 ^2) by Them5;
set z1 = (((x1 * y1) + (x2 * y2)) + (x3 * y3)) + (x4 * y4);
set z2 = (((- (x1 * y2)) + (x2 * y1)) - (x3 * y4)) + (x4 * y3);
set z3 = (((x1 * y3) - (x2 * y4)) - (x3 * y1)) + (x4 * y2);
set z4 = (((x1 * y4) + (x2 * y3)) - (x3 * y2)) - (x4 * y1);
reconsider n1 = |.((((x1 * y1) + (x2 * y2)) + (x3 * y3)) + (x4 * y4)).|, n2 = |.((((- (x1 * y2)) + (x2 * y1)) - (x3 * y4)) + (x4 * y3)).|, n3 = |.((((x1 * y3) - (x2 * y4)) - (x3 * y1)) + (x4 * y2)).|, n4 = |.((((x1 * y4) + (x2 * y3)) - (x3 * y2)) - (x4 * y1)).| as natural Number ;
reconsider n1 = n1, n2 = n2, n3 = n3, n4 = n4 as Nat by TARSKI:1;
A6: ( n1 ^2 = ((((x1 * y1) + (x2 * y2)) + (x3 * y3)) + (x4 * y4)) ^2 & n2 ^2 = ((((- (x1 * y2)) + (x2 * y1)) - (x3 * y4)) + (x4 * y3)) ^2 & n3 ^2 = ((((x1 * y3) - (x2 * y4)) - (x3 * y1)) + (x4 * y2)) ^2 & n4 ^2 = ((((x1 * y4) + (x2 * y3)) - (x3 * y2)) - (x4 * y1)) ^2 ) by COMPLEX1:75;
p |^ (n + 1) = (p |^ n) * p by NEWTON:6
.= (((((((x1 * y1) + (x2 * y2)) + (x3 * y3)) + (x4 * y4)) ^2) + (((((- (x1 * y2)) + (x2 * y1)) - (x3 * y4)) + (x4 * y3)) ^2)) + (((((x1 * y3) - (x2 * y4)) - (x3 * y1)) + (x4 * y2)) ^2)) + (((((x1 * y4) + (x2 * y3)) - (x3 * y2)) - (x4 * y1)) ^2) by A3, A4
.= (((n1 ^2) + (n2 ^2)) + (n3 ^2)) + (n4 ^2) by A6 ;
hence S₁[n + 1] ; :: thesis: verum

end;

A8: S₁[ 0 ]

proof

consider x1, x2, x3, x4 being Nat such that
A9: ( x1 = 1 & x2 = 0 & x3 = 0 & x4 = 0 ) ;
p |^ 0 = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2) by A9, NEWTON:4;
hence S₁[ 0 ] ; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A8, A1);
hence ex x1, x2, x3, x4 being Nat st p |^ n = (((x1 ^2) + (x2 ^2)) + (x3 ^2)) + (x4 ^2) ; :: thesis: verum