let y1, x1, x2 be Real; :: thesis: ( y1 > 0 & x1 >= 0 & x2 >= 0 implies (x1 * x2) to_power y1 = (x1 to_power y1) * (x2 to_power y1) )
assume A1: ( y1 > 0 & x1 >= 0 & 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 A1;

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:35; :: thesis: verum

end;

suppose A2: ( 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 A2; :: thesis: verum

end;

suppose A3: ( 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 A3; :: 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;

end;