let U1, U2 be preIfWhileAlgebra; :: thesis: ( UAStr(# the carrier of U1, the charact of U1 #) = UAStr(# the carrier of U2, the charact of U2 #) implies ElementaryInstructions U1 = ElementaryInstructions U2 )
assume A1: UAStr(# the carrier of U1, the charact of U1 #) = UAStr(# the carrier of U2, the charact of U2 #) ; :: thesis: ElementaryInstructions U1 = ElementaryInstructions U2
set Y1 = { (I1 \; I2) where I1, I2 is Algorithm of U1 : ( I1 <> I1 \; I2 & I2 <> I1 \; I2 ) } ;
set Y2 = { (I1 \; I2) where I1, I2 is Algorithm of U2 : ( I1 <> I1 \; I2 & I2 <> I1 \; I2 ) } ;
A2: { (I1 \; I2) where I1, I2 is Algorithm of U1 : ( I1 <> I1 \; I2 & I2 <> I1 \; I2 ) } = { (I1 \; I2) where I1, I2 is Algorithm of U2 : ( I1 <> I1 \; I2 & I2 <> I1 \; I2 ) }

proof

thus { (I1 \; I2) where I1, I2 is Algorithm of U1 : ( I1 <> I1 \; I2 & I2 <> I1 \; I2 ) } c= { (I1 \; I2) where I1, I2 is Algorithm of U2 : ( I1 <> I1 \; I2 & I2 <> I1 \; I2 ) } :: according to XBOOLE_0:def 10 :: thesis: { (I1 \; I2) where I1, I2 is Algorithm of U2 : ( I1 <> I1 \; I2 & I2 <> I1 \; I2 ) } c= { (I1 \; I2) where I1, I2 is Algorithm of U1 : ( I1 <> I1 \; I2 & I2 <> I1 \; I2 ) }

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (I1 \; I2) where I1, I2 is Algorithm of U1 : ( I1 <> I1 \; I2 & I2 <> I1 \; I2 ) } or x in { (I1 \; I2) where I1, I2 is Algorithm of U2 : ( I1 <> I1 \; I2 & I2 <> I1 \; I2 ) } )
assume x in { (I1 \; I2) where I1, I2 is Algorithm of U1 : ( I1 <> I1 \; I2 & I2 <> I1 \; I2 ) } ; :: thesis: x in { (I1 \; I2) where I1, I2 is Algorithm of U2 : ( I1 <> I1 \; I2 & I2 <> I1 \; I2 ) }
then consider I1, I2 being Algorithm of U1 such that
A3: ( x = I1 \; I2 & I1 <> I1 \; I2 & I2 <> I1 \; I2 ) ;
reconsider I1 = I1, I2 = I2 as Algorithm of U2 by A1;
x = I1 \; I2 by A1, A3;
hence x in { (I1 \; I2) where I1, I2 is Algorithm of U2 : ( I1 <> I1 \; I2 & I2 <> I1 \; I2 ) } by A3; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (I1 \; I2) where I1, I2 is Algorithm of U2 : ( I1 <> I1 \; I2 & I2 <> I1 \; I2 ) } or x in { (I1 \; I2) where I1, I2 is Algorithm of U1 : ( I1 <> I1 \; I2 & I2 <> I1 \; I2 ) } )
assume x in { (I1 \; I2) where I1, I2 is Algorithm of U2 : ( I1 <> I1 \; I2 & I2 <> I1 \; I2 ) } ; :: thesis: x in { (I1 \; I2) where I1, I2 is Algorithm of U1 : ( I1 <> I1 \; I2 & I2 <> I1 \; I2 ) }
then consider I1, I2 being Algorithm of U2 such that
A4: ( x = I1 \; I2 & I1 <> I1 \; I2 & I2 <> I1 \; I2 ) ;
reconsider I1 = I1, I2 = I2 as Algorithm of U1 by A1;
x = I1 \; I2 by A1, A4;
hence x in { (I1 \; I2) where I1, I2 is Algorithm of U1 : ( I1 <> I1 \; I2 & I2 <> I1 \; I2 ) } by A4; :: thesis: verum

end;

thus ElementaryInstructions U1 = ElementaryInstructions U2 by A2, A1; :: thesis: verum