set I = I_YG ;
A1: ( 1 / 2 in [.0,1.] & 1 in [.0,1.] ) by XXREAL_1:1;
BA: for x, y, z being Element of [.0,1.] holds I_YG . (x,(I_YG . (y,z))) = I_YG . (y,(I_YG . (x,z)))

proof

let x, y, z be Element of [.0,1.]; :: thesis: I_YG . (x,(I_YG . (y,z))) = I_YG . (y,(I_YG . (x,z)))

per cases ( ( x = 0 & y = 0 & z = 0 ) or z > 0 or ( y > 0 & x > 0 & z = 0 ) or ( y = 0 & x > 0 & z = 0 ) or ( y > 0 & x = 0 & z = 0 ) or ( y > 0 & x > 0 & z = 0 ) ) by XXREAL_1:1;

suppose Y0: ( x = 0 & y = 0 & z = 0 ) ; :: thesis: I_YG . (x,(I_YG . (y,z))) = I_YG . (y,(I_YG . (x,z)))

then Y1: I_YG . (x,(I_YG . (y,z))) = I_YG . (x,1) by FUZIMPL1:def 21
.= 1 to_power x by A1, FUZIMPL1:def 21
.= 1 by POWER:26 ;
I_YG . (y,(I_YG . (x,z))) = I_YG . (y,1) by FUZIMPL1:def 21, Y0
.= 1 to_power y by A1, FUZIMPL1:def 21
.= 1 by POWER:26 ;
hence I_YG . (x,(I_YG . (y,z))) = I_YG . (y,(I_YG . (x,z))) by Y1; :: thesis: verum

end;

suppose R1: z > 0 ; :: thesis: I_YG . (x,(I_YG . (y,z))) = I_YG . (y,(I_YG . (x,z)))

then r4: I_YG . (y,z) = z to_power y by FUZIMPL1:def 21;
r6: I_YG . (x,z) = z to_power x by R1, FUZIMPL1:def 21;
R2: z to_power y > 0 by R1, POWER:34;
R3: z to_power x > 0 by R1, POWER:34;
R5: I_YG . (x,(I_YG . (y,z))) = (z to_power y) to_power x by R2, r4, FUZIMPL1:def 21
.= z to_power (y * x) by R1, POWER:33 ;
I_YG . (y,(I_YG . (x,z))) = (z to_power x) to_power y by R3, r6, FUZIMPL1:def 21
.= z to_power (x * y) by R1, POWER:33 ;
hence I_YG . (x,(I_YG . (y,z))) = I_YG . (y,(I_YG . (x,z))) by R5; :: thesis: verum

end;

suppose R1: ( y > 0 & x > 0 & z = 0 ) ; :: thesis: I_YG . (x,(I_YG . (y,z))) = I_YG . (y,(I_YG . (x,z)))

then r4: I_YG . (y,z) = z to_power y by FUZIMPL1:def 21;
r6: I_YG . (x,z) = z to_power x by R1, FUZIMPL1:def 21;
R2: z to_power y = 0 by R1, POWER:def 2;
R3: z to_power x = 0 by R1, POWER:def 2;
R5: I_YG . (x,(I_YG . (y,z))) = (z to_power y) to_power x by R1, r4, FUZIMPL1:def 21
.= 0 by R1, POWER:def 2, R2 ;
I_YG . (y,(I_YG . (x,z))) = (z to_power x) to_power y by R1, r6, FUZIMPL1:def 21
.= 0 by R1, POWER:def 2, R3 ;
hence I_YG . (x,(I_YG . (y,z))) = I_YG . (y,(I_YG . (x,z))) by R5; :: thesis: verum

end;

suppose R1: ( y = 0 & x > 0 & z = 0 ) ; :: thesis: I_YG . (x,(I_YG . (y,z))) = I_YG . (y,(I_YG . (x,z)))

R3: z to_power x = 0 by R1, POWER:def 2;
R5: I_YG . (x,(I_YG . (y,z))) = I_YG . (x,1) by R1, FUZIMPL1:def 21
.= 1 to_power x by FUZIMPL1:def 21, A1
.= 1 by POWER:26 ;
I_YG . (y,(I_YG . (x,z))) = I_YG . (y,(z to_power x)) by R1, FUZIMPL1:def 21
.= 1 by R1, R3, FUZIMPL1:def 21 ;
hence I_YG . (x,(I_YG . (y,z))) = I_YG . (y,(I_YG . (x,z))) by R5; :: thesis: verum

end;

suppose R1: ( y > 0 & x = 0 & z = 0 ) ; :: thesis: I_YG . (x,(I_YG . (y,z))) = I_YG . (y,(I_YG . (x,z)))

then R2: z to_power y = 0 by POWER:def 2;
R5: I_YG . (x,(I_YG . (y,z))) = I_YG . (x,(z to_power y)) by R1, FUZIMPL1:def 21
.= 1 by R1, R2, FUZIMPL1:def 21 ;
I_YG . (y,(I_YG . (x,z))) = I_YG . (y,1) by R1, FUZIMPL1:def 21
.= 1 to_power y by FUZIMPL1:def 21, A1
.= 1 by POWER:26 ;
hence I_YG . (x,(I_YG . (y,z))) = I_YG . (y,(I_YG . (x,z))) by R5; :: thesis: verum

end;

suppose R1: ( y > 0 & x > 0 & z = 0 ) ; :: thesis: I_YG . (x,(I_YG . (y,z))) = I_YG . (y,(I_YG . (x,z)))

then r6: I_YG . (x,z) = z to_power x by FUZIMPL1:def 21;
R2: z to_power y = 0 by R1, POWER:def 2;
R3: z to_power x = 0 by R1, POWER:def 2;
R5: I_YG . (x,(I_YG . (y,z))) = I_YG . (x,(z to_power y)) by R1, FUZIMPL1:def 21
.= (z to_power y) to_power x by R1, R2, FUZIMPL1:def 21
.= 0 by R1, POWER:def 2, R2 ;
I_YG . (y,(I_YG . (x,z))) = (z to_power x) to_power y by R1, r6, FUZIMPL1:def 21
.= 0 by R1, POWER:def 2, R3 ;
hence I_YG . (x,(I_YG . (y,z))) = I_YG . (y,(I_YG . (x,z))) by R5; :: thesis: verum

end;

end;

end;

B2: for y being Element of [.0,1.] holds I_YG . (1,y) = y

proof

let y be Element of [.0,1.]; :: thesis: I_YG . (1,y) = y
I_YG . (1,y) = y to_power 1 by FUZIMPL1:def 21, A1;
hence I_YG . (1,y) = y by POWER:25; :: thesis: verum

end;

I_YG . ((1 / 2),(1 / 2)) = (1 / 2) to_power (1 / 2) by A1, FUZIMPL1:def 21;
hence ( I_YG is satisfying_(NP) & I_YG is satisfying_(EP) & not I_YG is satisfying_(IP) & not I_YG is satisfying_(OP) ) by BA, B2, A1, LemmaHalf; :: thesis: verum