let S be non empty set ; :: thesis:
let T be Subset of S; :: thesis:
let A be free ECIW-strict preIfWhileAlgebra; :: thesis:
let f1, f2 be ExecutionFunction of A,S,T; :: thesis:
assume A1: f1 | [:S,(ElementaryInstructions A):] = f2 | [:S,(ElementaryInstructions A):] ; :: thesis:
set g = f1 | [:S,(ElementaryInstructions A):];
assume A2: for s being Element of S
for C, I being Element of A st not f1 iteration_terminates_for I \; C,f1 . s,C holds
f1 . s,(while C,I) = f2 . s,(while C,I) ; :: thesis:
defpred S₁[ set ] means for s being Element of S holds f1 . s,$1 = f2 . s,$1;
A3: for I being Element of A st I in ElementaryInstructions A holds
S₁[I]

proof

let I be Element of A; :: thesis:
assume A4: I in ElementaryInstructions A ; :: thesis:
let s be Element of S; :: thesis:
A5: [s,I] in [:S,(ElementaryInstructions A):] by A4, ZFMISC_1:106;
hence f1 . s,I = (f1 | [:S,(ElementaryInstructions A):]) . [s,I] by FUNCT_1:72
.= f2 . s,I by A5, A1, FUNCT_1:72 ;
:: thesis:

end;

A6: S₁[ EmptyIns A]

proof

let s be Element of S; :: thesis:
thus f1 . s,(EmptyIns A) = s by Def28
.= f2 . s,(EmptyIns A) by Def28 ; :: thesis:

end;

A7: for I1, I2 being Element of A st S₁[I1] & S₁[I2] holds
S₁[I1 \; I2]

proof

let I1, I2 be Element of A; :: thesis:
assume A8: ( S₁[I1] & S₁[I2] ) ; :: thesis:
let s be Element of S; :: thesis:
thus f1 . s,(I1 \; I2) = f1 . (f1 . s,I1),I2 by Def29
.= f1 . (f2 . s,I1),I2 by A8
.= f2 . (f2 . s,I1),I2 by A8
.= f2 . s,(I1 \; I2) by Def29 ; :: thesis:

end;

A9: for C, I1, I2 being Element of A st S₁[C] & S₁[I1] & S₁[I2] holds
S₁[ if-then-else C,I1,I2]

proof

let C, I1, I2 be Element of A; :: thesis:
assume A10: ( S₁[C] & S₁[I1] & S₁[I2] ) ; :: thesis:
let s be Element of S; :: thesis:
A11: ( f1 complies_with_if_wrt T & f2 complies_with_if_wrt T ) by Def32;
A12: f1 . s,C = f2 . s,C by A10;

per cases ;

suppose A13: f1 . s,C in T ; :: thesis:

hence f1 . s,(if-then-else C,I1,I2) = f1 . (f1 . s,C),I1 by A11, Def30
.= f2 . (f1 . s,C),I1 by A10
.= f2 . s,(if-then-else C,I1,I2) by A11, A12, A13, Def30 ;
:: thesis:

end;

suppose A14: f1 . s,C nin T ; :: thesis:

hence f1 . s,(if-then-else C,I1,I2) = f1 . (f1 . s,C),I2 by A11, Def30
.= f2 . (f1 . s,C),I2 by A10
.= f2 . s,(if-then-else C,I1,I2) by A11, A12, A14, Def30 ;
:: thesis:

end;

A15: for C, I being Element of A st S₁[C] & S₁[I] holds
S₁[ while C,I]

proof

let C, I be Element of A; :: thesis:
assume A16: ( S₁[C] & S₁[I] ) ; :: thesis:
let s be Element of S; :: thesis:

now

assume f1 iteration_terminates_for I \; C,f1 . s,C ; :: thesis:
then consider r being non empty FinSequence of S such that
A17: ( r . 1 = f1 . s,C & r . (len r) nin T ) and
A18: for i being Nat st 1 <= i & i < len r holds
( r . i in T & r . (i + 1) = f1 . (r . i),(I \; C) ) by Def33;
A19: f1 . s,C = f2 . s,C by A16;

A20: now

let i be Nat; :: thesis:
assume A21: ( 1 <= i & i < len r ) ; :: thesis:
hence r . i in T by A18; :: thesis:
then reconsider si = r . i as Element of S ;
thus r . (i + 1) = f1 . si,(I \; C) by A18, A21
.= f1 . (f1 . si,I),C by Def29
.= f1 . (f2 . si,I),C by A16
.= f2 . (f2 . si,I),C by A16
.= f2 . (r . i),(I \; C) by Def29 ; :: thesis:

end;

thus f1 . s,(while C,I) = r . (len r) by A17, A18, Th86
.= f2 . s,(while C,I) by A17, A20, A19, Th86 ; :: thesis:

end;

hence f1 . s,(while C,I) = f2 . s,(while C,I) by A2; :: thesis:

end;

now

let sI be Element of [:S,the carrier of A:]; :: thesis:
consider s, I being set such that
A22: ( s in S & I in the carrier of A & sI = [s,I] ) by ZFMISC_1:def 2;
reconsider I = I as Element of A by A22;
reconsider s = s as Element of S by A22;
S₁[I] from AOFA_000:sch 2(A3, A6, A7, A9, A15);
then f1 . s,I = f2 . s,I ;
hence f1 . sI = f2 . sI by A22; :: thesis:

end;

hence f1 = f2 by FUNCT_2:113; :: thesis: