let x1, x2, y1 be Real; :: thesis: ( y1 > 0 & x1 >= 0 & x2 >= 0 implies (x1 * x2) to_power y1 = (x1 to_power y1) * (x2 to_power y1) )
assume that
A1: y1 > 0 and
A2: x1 >= 0 and
A3: x2 >= 0 ; :: thesis: (x1 * x2) to_power y1 = (x1 to_power y1) * (x2 to_power y1)

per cases ( ( x1 > 0 & x2 > 0 ) or ( x1 > 0 & x2 = 0 ) or ( x1 = 0 & x2 > 0 ) or ( x1 = 0 & x2 = 0 ) ) by A2, A3;

suppose ( x1 > 0 & x2 > 0 ) ; :: thesis: (x1 * x2) to_power y1 = (x1 to_power y1) * (x2 to_power y1)

hence (x1 * x2) to_power y1 = (x1 to_power y1) * (x2 to_power y1) by POWER:30; :: thesis: verum

end;

suppose A4: ( x1 > 0 & x2 = 0 ) ; :: thesis: (x1 * x2) to_power y1 = (x1 to_power y1) * (x2 to_power y1)

then x2 to_power y1 = 0 by A1, POWER:def 2;
hence (x1 * x2) to_power y1 = (x1 to_power y1) * (x2 to_power y1) by A4; :: thesis: verum

end;

suppose A5: ( x1 = 0 & x2 > 0 ) ; :: thesis: (x1 * x2) to_power y1 = (x1 to_power y1) * (x2 to_power y1)

then x1 to_power y1 = 0 by A1, POWER:def 2;
hence (x1 * x2) to_power y1 = (x1 to_power y1) * (x2 to_power y1) by A5; :: thesis: verum

end;

suppose A6: ( x1 = 0 & x2 = 0 ) ; :: thesis: (x1 * x2) to_power y1 = (x1 to_power y1) * (x2 to_power y1)

then x2 to_power y1 = 0 by A1, POWER:def 2;
hence (x1 * x2) to_power y1 = (x1 to_power y1) * (x2 to_power y1) by A6; :: thesis: verum

end;

end;