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 ;
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 ;
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 ;
hence (x1 * x2) to_power y1 = (x1 to_power y1) * (x2 to_power y1) by A6; :: thesis: verum
end;
end;