let U1, U2 be preIfWhileAlgebra; ( 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 #)
; 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 ) }
XBOOLE_0:def 10 { (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 ) }
let x be
object ;
TARSKI:def 3 ( 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 ) }
;
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;
verum
end;
thus
ElementaryInstructions U1 = ElementaryInstructions U2
by A2, A1; verum