let x, y be Real; :: thesis: ( x + y <> 0 implies (x + y) |^ 4 = ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * x) + ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * y) )
assume A1: x + y <> 0 ; :: thesis: (x + y) |^ 4 = ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * x) + ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * y)

per cases ( x + y > 0 or x + y < 0 ) by A1, XXREAL_0:1;

suppose A2: x + y > 0 ; :: thesis: (x + y) |^ 4 = ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * x) + ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * y)

(x + y) |^ 4 = (x + y) to_power (3 + 1) by POWER:41
.= ((x + y) to_power 3) * ((x + y) to_power 1) by A2, POWER:27
.= ((x + y) to_power 3) * (x + y) ;
then (x + y) |^ 4 = ((x + y) |^ 3) * (x + y)
.= (((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * (x + y) by POLYEQ_1:14 ;
hence (x + y) |^ 4 = ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * x) + ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * y) ; :: thesis: verum

end;

suppose x + y < 0 ; :: thesis: (x + y) |^ 4 = ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * x) + ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * y)

then A3: - (x + y) > 0 by XREAL_1:58;
(- (x + y)) |^ 4 = (x + y) |^ 4 by Lm1, POWER:1;
then (x + y) |^ 4 = (- (x + y)) to_power (3 + 1) by POWER:41
.= ((- (x + y)) to_power 3) * ((- (x + y)) to_power 1) by A3, POWER:27
.= ((- (x + y)) |^ 3) * ((- (x + y)) to_power 1) ;
then (x + y) |^ 4 = ((- (x + y)) |^ 3) * (- (x + y)) ;
then (x + y) |^ 4 = (- ((x + y) |^ 3)) * (- (x + y)) by Lm2, POWER:2
.= ((x + y) |^ 3) * (x + y)
.= (((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * (x + y) by POLYEQ_1:14 ;
hence (x + y) |^ 4 = ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * x) + ((((x |^ 3) + (((3 * y) * (x ^2)) + ((3 * (y ^2)) * x))) + (y |^ 3)) * y) ; :: thesis: verum

end;

end;