theorem :: AOFA_A00:42

for U1, U2 being preIfWhileAlgebra st UAStr(# the carrier of U1, the charact of U1 #) = UAStr(# the carrier of U2, the charact of U2 #) holds
( EmptyIns U1 = EmptyIns U2 & ( for I1, J1 being Element of U1
for I2, J2 being Element of U2 st I1 = I2 & J1 = J2 holds
( I1 \; J1 = I2 \; J2 & while (I1,J1) = while (I2,J2) & ( for C1 being Element of U1
for C2 being Element of U2 st C1 = C2 holds
if-then-else (C1,I1,J1) = if-then-else (C2,I2,J2) ) ) ) ) ;