set B = ElementaryInstructions F₁();
A2: (ElementaryInstructions F₁()) |^ 0 = ElementaryInstructions F₁() by Th18;
set FB = { [I,F₄(I)] where I is Element of F₁() : I in ElementaryInstructions F₁() } ;
deffunc H₁( Nat, set ) -> set = { [(I1 \; I2),F₅(fI1,fI2)] where I1, I2 is Element of F₁(), fI1, fI2 is Element of F₂() : ( I1 in (ElementaryInstructions F₁()) |^ $1 & I2 in (ElementaryInstructions F₁()) |^ $1 & [I1,fI1] in $2 & [I2,fI2] in $2 ) } ;
deffunc H₂( Nat, set ) -> set = { [(if-then-else (C,I1,I2)),F₇(fC,fI1,fI2)] where C, I1, I2 is Element of F₁(), fC, fI1, fI2 is Element of F₂() : ( C in (ElementaryInstructions F₁()) |^ $1 & I1 in (ElementaryInstructions F₁()) |^ $1 & I2 in (ElementaryInstructions F₁()) |^ $1 & [C,fC] in $2 & [I1,fI1] in $2 & [I2,fI2] in $2 ) } ;
deffunc H₃( Nat, set ) -> set = { [(while (C,I)),F₆(gC,gI)] where C, I is Element of F₁(), gC, gI is Element of F₂() : ( C in (ElementaryInstructions F₁()) |^ $1 & I in (ElementaryInstructions F₁()) |^ $1 & [C,gC] in $2 & [I,gI] in $2 ) } ;
deffunc H₄( Nat, set ) -> set = ((($2 \/ {[(EmptyIns F₁()),F₃()]}) \/ H₁($1,$2)) \/ H₂($1,$2)) \/ H₃($1,$2);
consider FF being Function such that
A3: ( dom FF = NAT & FF . 0 = { [I,F₄(I)] where I is Element of F₁() : I in ElementaryInstructions F₁() } ) and
A4: for n being Nat holds FF . (n + 1) = H₄(n,FF . n) from NAT_1:sch 11();
set f = Union FF;
A5: for n, m being Nat st n <= m holds
FF . n c= FF . m

proof

let n, m be Nat; :: thesis: ( n <= m implies FF . n c= FF . m )
assume n <= m ; :: thesis: FF . n c= FF . m
then consider i being Nat such that
A6: m = n + i by NAT_1:10;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
A7: m = n + i by A6;
defpred S₁[ Nat] means FF . n c= FF . (n + $1);
A8: S₁[ 0 ] ;

A9: now :: thesis: for i being Nat st S₁[i] holds
S₁[i + 1]

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
FF . ((n9 + i) + 1) = H₄(n9 + i,FF . (n9 + i)) by A4
.= (((FF . (n + i)) \/ {[(EmptyIns F₁()),F₃()]}) \/ H₁(n + i,FF . (n + i))) \/ (H₂(n + i,FF . (n + i)) \/ H₃(n + i,FF . (n + i))) by XBOOLE_1:4
.= ((FF . (n + i)) \/ {[(EmptyIns F₁()),F₃()]}) \/ (H₁(n + i,FF . (n + i)) \/ (H₂(n + i,FF . (n + i)) \/ H₃(n + i,FF . (n + i)))) by XBOOLE_1:4
.= (FF . (n + i)) \/ ({[(EmptyIns F₁()),F₃()]} \/ (H₁(n + i,FF . (n + i)) \/ (H₂(n + i,FF . (n + i)) \/ H₃(n + i,FF . (n + i))))) by XBOOLE_1:4 ;
then FF . (n + i) c= FF . ((n + i) + 1) by XBOOLE_1:7;
hence ( S₁[i] implies S₁[i + 1] ) by XBOOLE_1:1; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A8, A9);
hence FF . n c= FF . m by A7; :: thesis: verum

end;

defpred S₁[ Nat] means ex g being Function of ((ElementaryInstructions F₁()) |^ $1),F₂() st
( g = FF . $1 & ( EmptyIns F₁() in (ElementaryInstructions F₁()) |^ $1 implies g . (EmptyIns F₁()) = F₃() ) & ( for I1, I2 being Element of F₁() st I1 \; I2 in (ElementaryInstructions F₁()) |^ $1 holds
g . (I1 \; I2) = F₅((g . I1),(g . I2)) ) & ( for C, I1, I2 being Element of F₁() st if-then-else (C,I1,I2) in (ElementaryInstructions F₁()) |^ $1 holds
g . (if-then-else (C,I1,I2)) = F₇((g . C),(g . I1),(g . I2)) ) & ( for C, I being Element of F₁() st while (C,I) in (ElementaryInstructions F₁()) |^ $1 holds
g . (while (C,I)) = F₆((g . C),(g . I)) ) );
defpred S₂[ set ] means $1 in ElementaryInstructions F₁();
reconsider f0 = { [I,F₄(I)] where I is Element of F₁() : S₂[I] } as Function from ALTCAT_2:sch 1();
A10: dom f0 = ElementaryInstructions F₁()

proof

thus dom f0 c= ElementaryInstructions F₁() :: according to XBOOLE_0:def 10 :: thesis: ElementaryInstructions F₁() c= dom f0

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( x nin dom f0 or not x nin ElementaryInstructions F₁() )
assume x in dom f0 ; :: thesis: not x nin ElementaryInstructions F₁()
then [x,(f0 . x)] in f0 by FUNCT_1:def 2;
then ex I being Element of F₁() st
( [x,(f0 . x)] = [I,F₄(I)] & S₂[I] ) ;
hence not x nin ElementaryInstructions F₁() by XTUPLE_0:1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( x nin ElementaryInstructions F₁() or not x nin dom f0 )
assume A11: x in ElementaryInstructions F₁() ; :: thesis: not x nin dom f0
then reconsider I = x as Element of F₁() ;
[I,F₄(I)] in f0 by A11;
hence not x nin dom f0 by XTUPLE_0:def 12; :: thesis: verum

end;

rng f0 c= F₂()

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( y nin rng f0 or not y nin F₂() )
assume y in rng f0 ; :: thesis: not y nin F₂()
then consider x being object such that
A12: [x,y] in f0 by XTUPLE_0:def 13;
consider I being Element of F₁() such that
A13: [x,y] = [I,F₄(I)] and
A14: S₂[I] by A12;
y = F₄(I) by A13, XTUPLE_0:1;
hence not y nin F₂() by A1, A14; :: thesis: verum

end;

then reconsider f0 = f0 as Function of ((ElementaryInstructions F₁()) |^ 0),F₂() by A2, A10, FUNCT_2:2;
A15: S₁[ 0 ]

proof

take f0 ; :: thesis: ( f0 = FF . 0 & ( EmptyIns F₁() in (ElementaryInstructions F₁()) |^ 0 implies f0 . (EmptyIns F₁()) = F₃() ) & ( for I1, I2 being Element of F₁() st I1 \; I2 in (ElementaryInstructions F₁()) |^ 0 holds
f0 . (I1 \; I2) = F₅((f0 . I1),(f0 . I2)) ) & ( for C, I1, I2 being Element of F₁() st if-then-else (C,I1,I2) in (ElementaryInstructions F₁()) |^ 0 holds
f0 . (if-then-else (C,I1,I2)) = F₇((f0 . C),(f0 . I1),(f0 . I2)) ) & ( for C, I being Element of F₁() st while (C,I) in (ElementaryInstructions F₁()) |^ 0 holds
f0 . (while (C,I)) = F₆((f0 . C),(f0 . I)) ) )
thus f0 = FF . 0 by A3; :: thesis: ( ( EmptyIns F₁() in (ElementaryInstructions F₁()) |^ 0 implies f0 . (EmptyIns F₁()) = F₃() ) & ( for I1, I2 being Element of F₁() st I1 \; I2 in (ElementaryInstructions F₁()) |^ 0 holds
f0 . (I1 \; I2) = F₅((f0 . I1),(f0 . I2)) ) & ( for C, I1, I2 being Element of F₁() st if-then-else (C,I1,I2) in (ElementaryInstructions F₁()) |^ 0 holds
f0 . (if-then-else (C,I1,I2)) = F₇((f0 . C),(f0 . I1),(f0 . I2)) ) & ( for C, I being Element of F₁() st while (C,I) in (ElementaryInstructions F₁()) |^ 0 holds
f0 . (while (C,I)) = F₆((f0 . C),(f0 . I)) ) )

now :: thesis: for I1, I2 being Element of F₁() holds I1 \; I2 nin ElementaryInstructions F₁()

let I1, I2 be Element of F₁(); :: thesis: I1 \; I2 nin ElementaryInstructions F₁()
A16: I1 \; I2 <> I1 by Th73;
I1 \; I2 <> I2 by Th73;
hence I1 \; I2 nin ElementaryInstructions F₁() by A16, Th50; :: thesis: verum

end;

hence ( ( EmptyIns F₁() in (ElementaryInstructions F₁()) |^ 0 implies f0 . (EmptyIns F₁()) = F₃() ) & ( for I1, I2 being Element of F₁() st I1 \; I2 in (ElementaryInstructions F₁()) |^ 0 holds
f0 . (I1 \; I2) = F₅((f0 . I1),(f0 . I2)) ) & ( for C, I1, I2 being Element of F₁() st if-then-else (C,I1,I2) in (ElementaryInstructions F₁()) |^ 0 holds
f0 . (if-then-else (C,I1,I2)) = F₇((f0 . C),(f0 . I1),(f0 . I2)) ) & ( for C, I being Element of F₁() st while (C,I) in (ElementaryInstructions F₁()) |^ 0 holds
f0 . (while (C,I)) = F₆((f0 . C),(f0 . I)) ) ) by A2, Th49, Th51, Th52; :: thesis: verum

end;

A17: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
given g being Function of ((ElementaryInstructions F₁()) |^ i),F₂() such that A18: g = FF . i and
A19: ( EmptyIns F₁() in (ElementaryInstructions F₁()) |^ i implies g . (EmptyIns F₁()) = F₃() ) and
A20: for I1, I2 being Element of F₁() st I1 \; I2 in (ElementaryInstructions F₁()) |^ i holds
g . (I1 \; I2) = F₅((g . I1),(g . I2)) and
A21: for C, I1, I2 being Element of F₁() st if-then-else (C,I1,I2) in (ElementaryInstructions F₁()) |^ i holds
g . (if-then-else (C,I1,I2)) = F₇((g . C),(g . I1),(g . I2)) and
A22: for C, I being Element of F₁() st while (C,I) in (ElementaryInstructions F₁()) |^ i holds
g . (while (C,I)) = F₆((g . C),(g . I)) ; :: thesis: S₁[i + 1]
set h = FF . (i + 1);
A23: i < i + 1 by NAT_1:13;
A24: FF . (i + 1) = H₄(i,g) by A4, A18;
A25: dom g = (ElementaryInstructions F₁()) |^ i by FUNCT_2:def 1;
A26: (ElementaryInstructions F₁()) |^ i c= (ElementaryInstructions F₁()) |^ (i + 1) by A23, Th21;

A27: now :: thesis: for x being set holds
( not x in FF . (i + 1) or x in g or x in {[(EmptyIns F₁()),F₃()]} or x in H₁(i,g) or x in H₂(i,g) or x in H₃(i,g) )

let x be set ; :: thesis: ( not x in FF . (i + 1) or x in g or x in {[(EmptyIns F₁()),F₃()]} or x in H₁(i,g) or x in H₂(i,g) or x in H₃(i,g) )
assume x in FF . (i + 1) ; :: thesis: ( x in g or x in {[(EmptyIns F₁()),F₃()]} or x in H₁(i,g) or x in H₂(i,g) or x in H₃(i,g) )
then ( x in ((g \/ {[(EmptyIns F₁()),F₃()]}) \/ H₁(i,g)) \/ H₂(i,g) or x in H₃(i,g) ) by A24, XBOOLE_0:def 3;
then ( x in (g \/ {[(EmptyIns F₁()),F₃()]}) \/ H₁(i,g) or x in H₂(i,g) or x in H₃(i,g) ) by XBOOLE_0:def 3;
then ( x in g \/ {[(EmptyIns F₁()),F₃()]} or x in H₁(i,g) or x in H₂(i,g) or x in H₃(i,g) ) by XBOOLE_0:def 3;
hence ( x in g or x in {[(EmptyIns F₁()),F₃()]} or x in H₁(i,g) or x in H₂(i,g) or x in H₃(i,g) ) by XBOOLE_0:def 3; :: thesis: verum

end;

FF . (i + 1) is Relation-like

proof

let x be object ; :: according to RELAT_1:def 1 :: thesis: ( x nin FF . (i + 1) or ex b₁, b₂ being object st x = [b₁,b₂] )
assume x in FF . (i + 1) ; :: thesis: ex b₁, b₂ being object st x = [b₁,b₂]
then ( x in g or x in {[(EmptyIns F₁()),F₃()]} or x in H₁(i,g) or x in H₂(i,g) or x in H₃(i,g) ) by A27;
then ( ex a, b being object st x = [a,b] or x = [(EmptyIns F₁()),F₃()] or ex I1, I2 being Element of F₁() ex fI1, fI2 being Element of F₂() st
( x = [(I1 \; I2),F₅(fI1,fI2)] & I1 in (ElementaryInstructions F₁()) |^ i & I2 in (ElementaryInstructions F₁()) |^ i & [I1,fI1] in g & [I2,fI2] in g ) or ex C, I1, I2 being Element of F₁() ex a, b, c being Element of F₂() st
( x = [(if-then-else (C,I1,I2)),F₇(a,b,c)] & C in (ElementaryInstructions F₁()) |^ i & I1 in (ElementaryInstructions F₁()) |^ i & I2 in (ElementaryInstructions F₁()) |^ i & [C,a] in g & [I1,b] in g & [I2,c] in g ) or ex C, I being Element of F₁() ex a, b being Element of F₂() st
( x = [(while (C,I)),F₆(a,b)] & C in (ElementaryInstructions F₁()) |^ i & I in (ElementaryInstructions F₁()) |^ i & [C,a] in g & [I,b] in g ) ) by RELAT_1:def 1;
hence ex b₁, b₂ being object st x = [b₁,b₂] ; :: thesis: verum

end;

then reconsider h = FF . (i + 1) as Relation ;
h is Function-like

proof

let x, y1, y2 be object ; :: according to FUNCT_1:def 1 :: thesis: ( [x,y1] nin h or [x,y2] nin h or y1 = y2 )
set x1 = [x,y1];
set x2 = [x,y2];
assume A28: [x,y1] in h ; :: thesis: ( [x,y2] nin h or y1 = y2 )
assume A29: [x,y2] in h ; :: thesis: y1 = y2

per cases ( [x,y1] in g or [x,y1] in {[(EmptyIns F₁()),F₃()]} or [x,y1] in H₁(i,g) or [x,y1] in H₂(i,g) or [x,y1] in H₃(i,g) ) by A27, A28;

suppose A30: [x,y1] in g ; :: thesis: y1 = y2

then A31: x in dom g by FUNCT_1:1;
A32: y1 = g . x by A30, FUNCT_1:1;

per cases ( [x,y2] in g or [x,y2] in {[(EmptyIns F₁()),F₃()]} or [x,y2] in H₁(i,g) or [x,y2] in H₂(i,g) or [x,y2] in H₃(i,g) ) by A27, A29;

suppose [x,y2] in g ; :: thesis: y1 = y2

hence y1 = y2 by A30, FUNCT_1:def 1; :: thesis: verum

end;

suppose [x,y2] in {[(EmptyIns F₁()),F₃()]} ; :: thesis: y1 = y2

then A33: [x,y2] = [(EmptyIns F₁()),F₃()] by TARSKI:def 1;
then x = EmptyIns F₁() by XTUPLE_0:1;
hence y1 = y2 by A19, A31, A32, A33, XTUPLE_0:1; :: thesis: verum

end;

suppose [x,y2] in H₁(i,g) ; :: thesis: y1 = y2

then consider J1, J2 being Element of F₁(), gJ1, gJ2 being Element of F₂() such that
A34: [x,y2] = [(J1 \; J2),F₅(gJ1,gJ2)] and
J1 in (ElementaryInstructions F₁()) |^ i and
J2 in (ElementaryInstructions F₁()) |^ i and
A35: [J1,gJ1] in g and
A36: [J2,gJ2] in g ;
A37: x = J1 \; J2 by A34, XTUPLE_0:1;
A38: y2 = F₅(gJ1,gJ2) by A34, XTUPLE_0:1;
A39: g . J1 = gJ1 by A35, FUNCT_1:1;
g . J2 = gJ2 by A36, FUNCT_1:1;
hence y1 = y2 by A20, A31, A32, A37, A38, A39; :: thesis: verum

end;

suppose [x,y2] in H₂(i,g) ; :: thesis: y1 = y2

then consider D, J1, J2 being Element of F₁(), a, b, c being Element of F₂() such that
A40: [x,y2] = [(if-then-else (D,J1,J2)),F₇(a,b,c)] and
D in (ElementaryInstructions F₁()) |^ i and
J1 in (ElementaryInstructions F₁()) |^ i and
J2 in (ElementaryInstructions F₁()) |^ i and
A41: [D,a] in g and
A42: [J1,b] in g and
A43: [J2,c] in g ;
A44: x = if-then-else (D,J1,J2) by A40, XTUPLE_0:1;
A45: y2 = F₇(a,b,c) by A40, XTUPLE_0:1;
A46: g . D = a by A41, FUNCT_1:1;
A47: g . J1 = b by A42, FUNCT_1:1;
g . J2 = c by A43, FUNCT_1:1;
hence y1 = y2 by A21, A31, A32, A44, A45, A46, A47; :: thesis: verum

end;

suppose [x,y2] in H₃(i,g) ; :: thesis: y1 = y2

then consider D, J being Element of F₁(), a, b being Element of F₂() such that
A48: [x,y2] = [(while (D,J)),F₆(a,b)] and
D in (ElementaryInstructions F₁()) |^ i and
J in (ElementaryInstructions F₁()) |^ i and
A49: [D,a] in g and
A50: [J,b] in g ;
A51: x = while (D,J) by A48, XTUPLE_0:1;
A52: y2 = F₆(a,b) by A48, XTUPLE_0:1;
A53: g . D = a by A49, FUNCT_1:1;
g . J = b by A50, FUNCT_1:1;
hence y1 = y2 by A22, A31, A32, A51, A52, A53; :: thesis: verum

end;

end;

end;

suppose [x,y1] in {[(EmptyIns F₁()),F₃()]} ; :: thesis: y1 = y2

then A54: [x,y1] = [(EmptyIns F₁()),F₃()] by TARSKI:def 1;
then A55: x = EmptyIns F₁() by XTUPLE_0:1;
A56: y1 = F₃() by A54, XTUPLE_0:1;

per cases ( [x,y2] in g or [x,y2] in {[(EmptyIns F₁()),F₃()]} or [x,y2] in H₁(i,g) or [x,y2] in H₂(i,g) or [x,y2] in H₃(i,g) ) by A27, A29;

suppose A57: [x,y2] in g ; :: thesis: y1 = y2

then x in dom g by FUNCT_1:1;
hence y1 = y2 by A19, A55, A56, A57, FUNCT_1:1; :: thesis: verum

end;

suppose [x,y2] in {[(EmptyIns F₁()),F₃()]} ; :: thesis: y1 = y2

then [x,y2] = [(EmptyIns F₁()),F₃()] by TARSKI:def 1;
hence y1 = y2 by A54, XTUPLE_0:1; :: thesis: verum

end;

suppose [x,y2] in H₁(i,g) ; :: thesis: y1 = y2

then consider J1, J2 being Element of F₁(), a, b being Element of F₂() such that
A58: [x,y2] = [(J1 \; J2),F₅(a,b)] and
J1 in (ElementaryInstructions F₁()) |^ i and
J2 in (ElementaryInstructions F₁()) |^ i and
[J1,a] in g and
[J2,b] in g ;
x = J1 \; J2 by A58, XTUPLE_0:1;
hence y1 = y2 by A55, Th72; :: thesis: verum

end;

suppose [x,y2] in H₂(i,g) ; :: thesis: y1 = y2

then consider D, J1, J2 being Element of F₁(), a, b, c being Element of F₂() such that
A59: [x,y2] = [(if-then-else (D,J1,J2)),F₇(a,b,c)] and
D in (ElementaryInstructions F₁()) |^ i and
J1 in (ElementaryInstructions F₁()) |^ i and
J2 in (ElementaryInstructions F₁()) |^ i and
[D,a] in g and
[J1,b] in g and
[J2,c] in g ;
x = if-then-else (D,J1,J2) by A59, XTUPLE_0:1;
hence y1 = y2 by A55, Def24; :: thesis: verum

end;

suppose [x,y2] in H₃(i,g) ; :: thesis: y1 = y2

then consider D, J being Element of F₁(), a, b being Element of F₂() such that
A60: [x,y2] = [(while (D,J)),F₆(a,b)] and
D in (ElementaryInstructions F₁()) |^ i and
J in (ElementaryInstructions F₁()) |^ i and
[D,a] in g and
[J,b] in g ;
x = while (D,J) by A60, XTUPLE_0:1;
hence y1 = y2 by A55, Def24; :: thesis: verum

end;

end;

end;

suppose [x,y1] in H₁(i,g) ; :: thesis: y1 = y2

then consider I1, I2 being Element of F₁(), gI1, gI2 being Element of F₂() such that
A61: [x,y1] = [(I1 \; I2),F₅(gI1,gI2)] and
I1 in (ElementaryInstructions F₁()) |^ i and
I2 in (ElementaryInstructions F₁()) |^ i and
A62: [I1,gI1] in g and
A63: [I2,gI2] in g ;
A64: x = I1 \; I2 by A61, XTUPLE_0:1;
A65: y1 = F₅(gI1,gI2) by A61, XTUPLE_0:1;
A66: g . I1 = gI1 by A62, FUNCT_1:1;
A67: g . I2 = gI2 by A63, FUNCT_1:1;

per cases ( [x,y2] in g or [x,y2] in {[(EmptyIns F₁()),F₃()]} or [x,y2] in H₁(i,g) or [x,y2] in H₂(i,g) or [x,y2] in H₃(i,g) ) by A27, A29;

suppose A68: [x,y2] in g ; :: thesis: y1 = y2

then A69: x in dom g by FUNCT_1:1;
y2 = g . x by A68, FUNCT_1:1;
hence y1 = y2 by A20, A64, A65, A66, A67, A69; :: thesis: verum

end;

suppose [x,y2] in {[(EmptyIns F₁()),F₃()]} ; :: thesis: y1 = y2

then [x,y2] = [(EmptyIns F₁()),F₃()] by TARSKI:def 1;
then x = EmptyIns F₁() by XTUPLE_0:1;
hence y1 = y2 by A64, Th72; :: thesis: verum

end;

suppose [x,y2] in H₁(i,g) ; :: thesis: y1 = y2

then consider J1, J2 being Element of F₁(), a, b being Element of F₂() such that
A70: [x,y2] = [(J1 \; J2),F₅(a,b)] and
J1 in (ElementaryInstructions F₁()) |^ i and
J2 in (ElementaryInstructions F₁()) |^ i and
A71: [J1,a] in g and
A72: [J2,b] in g ;
A73: x = J1 \; J2 by A70, XTUPLE_0:1;
A74: y2 = F₅(a,b) by A70, XTUPLE_0:1;
A75: g . J1 = a by A71, FUNCT_1:1;
A76: g . J2 = b by A72, FUNCT_1:1;
I1 = J1 by A64, A73, Th73;
hence y1 = y2 by A64, A65, A66, A67, A73, A74, A75, A76, Th73; :: thesis: verum

end;

suppose [x,y2] in H₂(i,g) ; :: thesis: y1 = y2

then consider D, J1, J2 being Element of F₁(), a, b, c being Element of F₂() such that
A77: [x,y2] = [(if-then-else (D,J1,J2)),F₇(a,b,c)] and
D in (ElementaryInstructions F₁()) |^ i and
J1 in (ElementaryInstructions F₁()) |^ i and
J2 in (ElementaryInstructions F₁()) |^ i and
[D,a] in g and
[J1,b] in g and
[J2,c] in g ;
x = if-then-else (D,J1,J2) by A77, XTUPLE_0:1;
hence y1 = y2 by A64, Th73; :: thesis: verum

end;

suppose [x,y2] in H₃(i,g) ; :: thesis: y1 = y2

then consider D, J being Element of F₁(), a, b being Element of F₂() such that
A78: [x,y2] = [(while (D,J)),F₆(a,b)] and
D in (ElementaryInstructions F₁()) |^ i and
J in (ElementaryInstructions F₁()) |^ i and
[D,a] in g and
[J,b] in g ;
x = while (D,J) by A78, XTUPLE_0:1;
hence y1 = y2 by A64, Th73; :: thesis: verum

end;

end;

end;

suppose [x,y1] in H₂(i,g) ; :: thesis: y1 = y2

then consider C, I1, I2 being Element of F₁(), gC, gI1, gI2 being Element of F₂() such that
A79: [x,y1] = [(if-then-else (C,I1,I2)),F₇(gC,gI1,gI2)] and
C in (ElementaryInstructions F₁()) |^ i and
I1 in (ElementaryInstructions F₁()) |^ i and
I2 in (ElementaryInstructions F₁()) |^ i and
A80: [C,gC] in g and
A81: [I1,gI1] in g and
A82: [I2,gI2] in g ;
A83: x = if-then-else (C,I1,I2) by A79, XTUPLE_0:1;
A84: y1 = F₇(gC,gI1,gI2) by A79, XTUPLE_0:1;
A85: g . I1 = gI1 by A81, FUNCT_1:1;
A86: g . I2 = gI2 by A82, FUNCT_1:1;
A87: g . C = gC by A80, FUNCT_1:1;

per cases ( [x,y2] in g or [x,y2] in {[(EmptyIns F₁()),F₃()]} or [x,y2] in H₁(i,g) or [x,y2] in H₂(i,g) or [x,y2] in H₃(i,g) ) by A27, A29;

suppose A88: [x,y2] in g ; :: thesis: y1 = y2

then A89: x in dom g by FUNCT_1:1;
y2 = g . x by A88, FUNCT_1:1;
hence y1 = y2 by A21, A83, A84, A85, A86, A87, A89; :: thesis: verum

end;

suppose [x,y2] in {[(EmptyIns F₁()),F₃()]} ; :: thesis: y1 = y2

then [x,y2] = [(EmptyIns F₁()),F₃()] by TARSKI:def 1;
then x = EmptyIns F₁() by XTUPLE_0:1;
hence y1 = y2 by A83, Th72; :: thesis: verum

end;

suppose [x,y2] in H₁(i,g) ; :: thesis: y1 = y2

then consider J1, J2 being Element of F₁(), a, b being Element of F₂() such that
A90: [x,y2] = [(J1 \; J2),F₅(a,b)] and
J1 in (ElementaryInstructions F₁()) |^ i and
J2 in (ElementaryInstructions F₁()) |^ i and
[J1,a] in g and
[J2,b] in g ;
x = J1 \; J2 by A90, XTUPLE_0:1;
hence y1 = y2 by A83, Th73; :: thesis: verum

end;

suppose [x,y2] in H₂(i,g) ; :: thesis: y1 = y2

then consider D, J1, J2 being Element of F₁(), a, b, c being Element of F₂() such that
A91: [x,y2] = [(if-then-else (D,J1,J2)),F₇(a,b,c)] and
D in (ElementaryInstructions F₁()) |^ i and
J1 in (ElementaryInstructions F₁()) |^ i and
J2 in (ElementaryInstructions F₁()) |^ i and
A92: [D,a] in g and
A93: [J1,b] in g and
A94: [J2,c] in g ;
A95: x = if-then-else (D,J1,J2) by A91, XTUPLE_0:1;
A96: y2 = F₇(a,b,c) by A91, XTUPLE_0:1;
A97: g . D = a by A92, FUNCT_1:1;
A98: g . J1 = b by A93, FUNCT_1:1;
A99: g . J2 = c by A94, FUNCT_1:1;
A100: C = D by A83, A95, Th74;
I1 = J1 by A83, A95, Th74;
hence y1 = y2 by A83, A84, A85, A86, A87, A95, A96, A97, A98, A99, A100, Th74; :: thesis: verum

end;

suppose [x,y2] in H₃(i,g) ; :: thesis: y1 = y2

then consider D, J being Element of F₁(), a, b being Element of F₂() such that
A101: [x,y2] = [(while (D,J)),F₆(a,b)] and
D in (ElementaryInstructions F₁()) |^ i and
J in (ElementaryInstructions F₁()) |^ i and
[D,a] in g and
[J,b] in g ;
x = while (D,J) by A101, XTUPLE_0:1;
hence y1 = y2 by A83, Th74; :: thesis: verum

end;

end;

end;

suppose [x,y1] in H₃(i,g) ; :: thesis: y1 = y2

then consider C, I being Element of F₁(), gC, gI being Element of F₂() such that
A102: [x,y1] = [(while (C,I)),F₆(gC,gI)] and
C in (ElementaryInstructions F₁()) |^ i and
I in (ElementaryInstructions F₁()) |^ i and
A103: [C,gC] in g and
A104: [I,gI] in g ;
A105: x = while (C,I) by A102, XTUPLE_0:1;
A106: y1 = F₆(gC,gI) by A102, XTUPLE_0:1;
A107: g . C = gC by A103, FUNCT_1:1;
A108: g . I = gI by A104, FUNCT_1:1;

per cases ( [x,y2] in g or [x,y2] in {[(EmptyIns F₁()),F₃()]} or [x,y2] in H₁(i,g) or [x,y2] in H₂(i,g) or [x,y2] in H₃(i,g) ) by A27, A29;

suppose A109: [x,y2] in g ; :: thesis: y1 = y2

then A110: x in dom g by FUNCT_1:1;
y2 = g . x by A109, FUNCT_1:1;
hence y1 = y2 by A22, A105, A106, A107, A108, A110; :: thesis: verum

end;

suppose [x,y2] in {[(EmptyIns F₁()),F₃()]} ; :: thesis: y1 = y2

then [x,y2] = [(EmptyIns F₁()),F₃()] by TARSKI:def 1;
then x = EmptyIns F₁() by XTUPLE_0:1;
hence y1 = y2 by A105, Th72; :: thesis: verum

end;

suppose [x,y2] in H₁(i,g) ; :: thesis: y1 = y2

then consider J1, J2 being Element of F₁(), a, b being Element of F₂() such that
A111: [x,y2] = [(J1 \; J2),F₅(a,b)] and
J1 in (ElementaryInstructions F₁()) |^ i and
J2 in (ElementaryInstructions F₁()) |^ i and
[J1,a] in g and
[J2,b] in g ;
x = J1 \; J2 by A111, XTUPLE_0:1;
hence y1 = y2 by A105, Th73; :: thesis: verum

end;

suppose [x,y2] in H₂(i,g) ; :: thesis: y1 = y2

then consider D, J1, J2 being Element of F₁(), a, b, c being Element of F₂() such that
A112: [x,y2] = [(if-then-else (D,J1,J2)),F₇(a,b,c)] and
D in (ElementaryInstructions F₁()) |^ i and
J1 in (ElementaryInstructions F₁()) |^ i and
J2 in (ElementaryInstructions F₁()) |^ i and
[D,a] in g and
[J1,b] in g and
[J2,c] in g ;
x = if-then-else (D,J1,J2) by A112, XTUPLE_0:1;
hence y1 = y2 by A105, Th74; :: thesis: verum

end;

suppose [x,y2] in H₃(i,g) ; :: thesis: y1 = y2

then consider D, J being Element of F₁(), a, b being Element of F₂() such that
A113: [x,y2] = [(while (D,J)),F₆(a,b)] and
D in (ElementaryInstructions F₁()) |^ i and
J in (ElementaryInstructions F₁()) |^ i and
A114: [D,a] in g and
A115: [J,b] in g ;
A116: x = while (D,J) by A113, XTUPLE_0:1;
A117: y2 = F₆(a,b) by A113, XTUPLE_0:1;
A118: g . D = a by A114, FUNCT_1:1;
A119: g . J = b by A115, FUNCT_1:1;
D = C by A105, A116, Th75;
hence y1 = y2 by A105, A106, A107, A108, A116, A117, A118, A119, Th75; :: thesis: verum

end;

end;

end;

end;

end;

then reconsider h = h as Function ;
A120: dom h = (ElementaryInstructions F₁()) |^ (i + 1)

proof

thus dom h c= (ElementaryInstructions F₁()) |^ (i + 1) :: according to XBOOLE_0:def 10 :: thesis: (ElementaryInstructions F₁()) |^ (i + 1) c= dom h

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( a nin dom h or not a nin (ElementaryInstructions F₁()) |^ (i + 1) )
set ah = [a,(h . a)];
assume a in dom h ; :: thesis: not a nin (ElementaryInstructions F₁()) |^ (i + 1)
then A121: [a,(h . a)] in h by FUNCT_1:def 2;

per cases ( [a,(h . a)] in g or [a,(h . a)] in {[(EmptyIns F₁()),F₃()]} or [a,(h . a)] in H₁(i,g) or [a,(h . a)] in H₂(i,g) or [a,(h . a)] in H₃(i,g) ) by A27, A121;

suppose [a,(h . a)] in g ; :: thesis: not a nin (ElementaryInstructions F₁()) |^ (i + 1)

then a in dom g by FUNCT_1:1;
hence not a nin (ElementaryInstructions F₁()) |^ (i + 1) by A26; :: thesis: verum

end;

suppose [a,(h . a)] in {[(EmptyIns F₁()),F₃()]} ; :: thesis: not a nin (ElementaryInstructions F₁()) |^ (i + 1)

then [a,(h . a)] = [(EmptyIns F₁()),F₃()] by TARSKI:def 1;
then a = EmptyIns F₁() by XTUPLE_0:1;
hence not a nin (ElementaryInstructions F₁()) |^ (i + 1) by Th76; :: thesis: verum

end;

suppose [a,(h . a)] in H₁(i,g) ; :: thesis: not a nin (ElementaryInstructions F₁()) |^ (i + 1)

then consider I, J being Element of F₁(), e, b being Element of F₂() such that
A122: [a,(h . a)] = [(I \; J),F₅(e,b)] and
A123: I in (ElementaryInstructions F₁()) |^ i and
A124: J in (ElementaryInstructions F₁()) |^ i and
[I,e] in g and
[J,b] in g ;
a = I \; J by A122, XTUPLE_0:1;
hence not a nin (ElementaryInstructions F₁()) |^ (i + 1) by A123, A124, Th76; :: thesis: verum

end;

suppose [a,(h . a)] in H₂(i,g) ; :: thesis: not a nin (ElementaryInstructions F₁()) |^ (i + 1)

then consider C, I, J being Element of F₁(), e, b, c being Element of F₂() such that
A125: [a,(h . a)] = [(if-then-else (C,I,J)),F₇(e,b,c)] and
A126: C in (ElementaryInstructions F₁()) |^ i and
A127: I in (ElementaryInstructions F₁()) |^ i and
A128: J in (ElementaryInstructions F₁()) |^ i and
[C,e] in g and
[I,b] in g and
[J,c] in g ;
a = if-then-else (C,I,J) by A125, XTUPLE_0:1;
hence not a nin (ElementaryInstructions F₁()) |^ (i + 1) by A126, A127, A128, Th76; :: thesis: verum

end;

suppose [a,(h . a)] in H₃(i,g) ; :: thesis: not a nin (ElementaryInstructions F₁()) |^ (i + 1)

then consider I, J being Element of F₁(), e, b being Element of F₂() such that
A129: [a,(h . a)] = [(while (I,J)),F₆(e,b)] and
A130: I in (ElementaryInstructions F₁()) |^ i and
A131: J in (ElementaryInstructions F₁()) |^ i and
[I,e] in g and
[J,b] in g ;
a = while (I,J) by A129, XTUPLE_0:1;
hence not a nin (ElementaryInstructions F₁()) |^ (i + 1) by A130, A131, Th76; :: thesis: verum

end;

end;

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( x nin (ElementaryInstructions F₁()) |^ (i + 1) or not x nin dom h )
assume A132: x in (ElementaryInstructions F₁()) |^ (i + 1) ; :: thesis: not x nin dom h

per cases ( x in (ElementaryInstructions F₁()) |^ i or x = EmptyIns F₁() or ex I1, I2 being Element of F₁() st
( x = I1 \; I2 & I1 in (ElementaryInstructions F₁()) |^ i & I2 in (ElementaryInstructions F₁()) |^ i ) or ex C, I1, I2 being Element of F₁() st
( x = if-then-else (C,I1,I2) & C in (ElementaryInstructions F₁()) |^ i & I1 in (ElementaryInstructions F₁()) |^ i & I2 in (ElementaryInstructions F₁()) |^ i ) or ex C, I being Element of F₁() st
( x = while (C,I) & C in (ElementaryInstructions F₁()) |^ i & I in (ElementaryInstructions F₁()) |^ i ) ) by A132, Th77;

suppose x in (ElementaryInstructions F₁()) |^ i ; :: thesis: not x nin dom h

then [x,(g . x)] in g by A25, FUNCT_1:def 2;
then [x,(g . x)] in g \/ {[(EmptyIns F₁()),F₃()]} by XBOOLE_0:def 3;
then [x,(g . x)] in (g \/ {[(EmptyIns F₁()),F₃()]}) \/ H₁(i,g) by XBOOLE_0:def 3;
then [x,(g . x)] in ((g \/ {[(EmptyIns F₁()),F₃()]}) \/ H₁(i,g)) \/ H₂(i,g) by XBOOLE_0:def 3;
then [x,(g . x)] in h by A24, XBOOLE_0:def 3;
hence not x nin dom h by XTUPLE_0:def 12; :: thesis: verum

end;

suppose x = EmptyIns F₁() ; :: thesis: not x nin dom h

then [x,F₃()] in {[(EmptyIns F₁()),F₃()]} by TARSKI:def 1;
then [x,F₃()] in g \/ {[(EmptyIns F₁()),F₃()]} by XBOOLE_0:def 3;
then [x,F₃()] in (g \/ {[(EmptyIns F₁()),F₃()]}) \/ H₁(i,g) by XBOOLE_0:def 3;
then [x,F₃()] in ((g \/ {[(EmptyIns F₁()),F₃()]}) \/ H₁(i,g)) \/ H₂(i,g) by XBOOLE_0:def 3;
then [x,F₃()] in h by A24, XBOOLE_0:def 3;
hence not x nin dom h by XTUPLE_0:def 12; :: thesis: verum

end;

suppose ex I1, I2 being Element of F₁() st
( x = I1 \; I2 & I1 in (ElementaryInstructions F₁()) |^ i & I2 in (ElementaryInstructions F₁()) |^ i ) ; :: thesis: not x nin dom h

then consider I1, I2 being Element of F₁() such that
A133: x = I1 \; I2 and
A134: I1 in (ElementaryInstructions F₁()) |^ i and
A135: I2 in (ElementaryInstructions F₁()) |^ i ;
reconsider a = g . I1, b = g . I2 as Element of F₂() by A134, A135, FUNCT_2:5;
A136: [I1,a] in g by A25, A134, FUNCT_1:def 2;
[I2,b] in g by A25, A135, FUNCT_1:def 2;
then [x,F₅(a,b)] in H₁(i,g) by A133, A134, A135, A136;
then [x,F₅(a,b)] in (g \/ {[(EmptyIns F₁()),F₃()]}) \/ H₁(i,g) by XBOOLE_0:def 3;
then [x,F₅(a,b)] in ((g \/ {[(EmptyIns F₁()),F₃()]}) \/ H₁(i,g)) \/ H₂(i,g) by XBOOLE_0:def 3;
then [x,F₅(a,b)] in h by A24, XBOOLE_0:def 3;
hence not x nin dom h by XTUPLE_0:def 12; :: thesis: verum

end;

suppose ex C, I1, I2 being Element of F₁() st
( x = if-then-else (C,I1,I2) & C in (ElementaryInstructions F₁()) |^ i & I1 in (ElementaryInstructions F₁()) |^ i & I2 in (ElementaryInstructions F₁()) |^ i ) ; :: thesis: not x nin dom h

then consider C, I1, I2 being Element of F₁() such that
A137: x = if-then-else (C,I1,I2) and
A138: C in (ElementaryInstructions F₁()) |^ i and
A139: I1 in (ElementaryInstructions F₁()) |^ i and
A140: I2 in (ElementaryInstructions F₁()) |^ i ;
reconsider a = g . I1, b = g . I2, c = g . C as Element of F₂() by A138, A139, A140, FUNCT_2:5;
A141: [I1,a] in g by A25, A139, FUNCT_1:def 2;
A142: [I2,b] in g by A25, A140, FUNCT_1:def 2;
[C,c] in g by A25, A138, FUNCT_1:def 2;
then [x,F₇(c,a,b)] in H₂(i,g) by A137, A138, A139, A140, A141, A142;
then [x,F₇(c,a,b)] in ((g \/ {[(EmptyIns F₁()),F₃()]}) \/ H₁(i,g)) \/ H₂(i,g) by XBOOLE_0:def 3;
then [x,F₇(c,a,b)] in h by A24, XBOOLE_0:def 3;
hence not x nin dom h by XTUPLE_0:def 12; :: thesis: verum

end;

suppose ex C, I being Element of F₁() st
( x = while (C,I) & C in (ElementaryInstructions F₁()) |^ i & I in (ElementaryInstructions F₁()) |^ i ) ; :: thesis: not x nin dom h

then consider C, I being Element of F₁() such that
A143: x = while (C,I) and
A144: C in (ElementaryInstructions F₁()) |^ i and
A145: I in (ElementaryInstructions F₁()) |^ i ;
reconsider a = g . C, b = g . I as Element of F₂() by A144, A145, FUNCT_2:5;
A146: [C,a] in g by A25, A144, FUNCT_1:def 2;
[I,b] in g by A25, A145, FUNCT_1:def 2;
then [x,F₆(a,b)] in H₃(i,g) by A143, A144, A145, A146;
then [x,F₆(a,b)] in h by A24, XBOOLE_0:def 3;
hence not x nin dom h by XTUPLE_0:def 12; :: thesis: verum

end;

end;

end;

rng h c= F₂()

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( a nin rng h or not a nin F₂() )
assume a in rng h ; :: thesis: not a nin F₂()
then consider x being object such that
A147: [x,a] in h by XTUPLE_0:def 13;
set ah = [x,a];

per cases ( [x,a] in g or [x,a] in {[(EmptyIns F₁()),F₃()]} or [x,a] in H₁(i,g) or [x,a] in H₂(i,g) or [x,a] in H₃(i,g) ) by A27, A147;

suppose [x,a] in g ; :: thesis: not a nin F₂()

hence not a nin F₂() by ZFMISC_1:87; :: thesis: verum

end;

suppose [x,a] in {[(EmptyIns F₁()),F₃()]} ; :: thesis: not a nin F₂()

then [x,a] = [(EmptyIns F₁()),F₃()] by TARSKI:def 1;
then a = F₃() by XTUPLE_0:1;
hence not a nin F₂() ; :: thesis: verum

end;

suppose [x,a] in H₁(i,g) ; :: thesis: not a nin F₂()

then consider I, J being Element of F₁(), e, b being Element of F₂() such that
A148: [x,a] = [(I \; J),F₅(e,b)] and
I in (ElementaryInstructions F₁()) |^ i and
J in (ElementaryInstructions F₁()) |^ i and
[I,e] in g and
[J,b] in g ;
a = F₅(e,b) by A148, XTUPLE_0:1;
hence not a nin F₂() ; :: thesis: verum

end;

suppose [x,a] in H₂(i,g) ; :: thesis: not a nin F₂()

then consider C, I, J being Element of F₁(), e, b, c being Element of F₂() such that
A149: [x,a] = [(if-then-else (C,I,J)),F₇(e,b,c)] and
C in (ElementaryInstructions F₁()) |^ i and
I in (ElementaryInstructions F₁()) |^ i and
J in (ElementaryInstructions F₁()) |^ i and
[C,e] in g and
[I,b] in g and
[J,c] in g ;
a = F₇(e,b,c) by A149, XTUPLE_0:1;
hence not a nin F₂() ; :: thesis: verum

end;

suppose [x,a] in H₃(i,g) ; :: thesis: not a nin F₂()

then consider I, J being Element of F₁(), e, b being Element of F₂() such that
A150: [x,a] = [(while (I,J)),F₆(e,b)] and
I in (ElementaryInstructions F₁()) |^ i and
J in (ElementaryInstructions F₁()) |^ i and
[I,e] in g and
[J,b] in g ;
a = F₆(e,b) by A150, XTUPLE_0:1;
hence not a nin F₂() ; :: thesis: verum

end;

end;

end;

then reconsider h = h as Function of ((ElementaryInstructions F₁()) |^ (i + 1)),F₂() by A120, FUNCT_2:2;
h = ((g \/ {[(EmptyIns F₁()),F₃()]}) \/ H₁(i,g)) \/ (H₂(i,g) \/ H₃(i,g)) by A24, XBOOLE_1:4
.= (g \/ {[(EmptyIns F₁()),F₃()]}) \/ (H₁(i,g) \/ (H₂(i,g) \/ H₃(i,g))) by XBOOLE_1:4
.= g \/ ({[(EmptyIns F₁()),F₃()]} \/ (H₁(i,g) \/ (H₂(i,g) \/ H₃(i,g)))) by XBOOLE_1:4 ;
then A151: g c= h by XBOOLE_1:7;
take h ; :: thesis: ( h = FF . (i + 1) & ( EmptyIns F₁() in (ElementaryInstructions F₁()) |^ (i + 1) implies h . (EmptyIns F₁()) = F₃() ) & ( for I1, I2 being Element of F₁() st I1 \; I2 in (ElementaryInstructions F₁()) |^ (i + 1) holds
h . (I1 \; I2) = F₅((h . I1),(h . I2)) ) & ( for C, I1, I2 being Element of F₁() st if-then-else (C,I1,I2) in (ElementaryInstructions F₁()) |^ (i + 1) holds
h . (if-then-else (C,I1,I2)) = F₇((h . C),(h . I1),(h . I2)) ) & ( for C, I being Element of F₁() st while (C,I) in (ElementaryInstructions F₁()) |^ (i + 1) holds
h . (while (C,I)) = F₆((h . C),(h . I)) ) )
thus h = FF . (i + 1) ; :: thesis: ( ( EmptyIns F₁() in (ElementaryInstructions F₁()) |^ (i + 1) implies h . (EmptyIns F₁()) = F₃() ) & ( for I1, I2 being Element of F₁() st I1 \; I2 in (ElementaryInstructions F₁()) |^ (i + 1) holds
h . (I1 \; I2) = F₅((h . I1),(h . I2)) ) & ( for C, I1, I2 being Element of F₁() st if-then-else (C,I1,I2) in (ElementaryInstructions F₁()) |^ (i + 1) holds
h . (if-then-else (C,I1,I2)) = F₇((h . C),(h . I1),(h . I2)) ) & ( for C, I being Element of F₁() st while (C,I) in (ElementaryInstructions F₁()) |^ (i + 1) holds
h . (while (C,I)) = F₆((h . C),(h . I)) ) )

hereby :: thesis: ( ( for I1, I2 being Element of F₁() st I1 \; I2 in (ElementaryInstructions F₁()) |^ (i + 1) holds
h . (I1 \; I2) = F₅((h . I1),(h . I2)) ) & ( for C, I1, I2 being Element of F₁() st if-then-else (C,I1,I2) in (ElementaryInstructions F₁()) |^ (i + 1) holds
h . (if-then-else (C,I1,I2)) = F₇((h . C),(h . I1),(h . I2)) ) & ( for C, I being Element of F₁() st while (C,I) in (ElementaryInstructions F₁()) |^ (i + 1) holds
h . (while (C,I)) = F₆((h . C),(h . I)) ) )

set x = EmptyIns F₁();
assume EmptyIns F₁() in (ElementaryInstructions F₁()) |^ (i + 1) ; :: thesis: h . (EmptyIns F₁()) = F₃()
[(EmptyIns F₁()),F₃()] in {[(EmptyIns F₁()),F₃()]} by TARSKI:def 1;
then [(EmptyIns F₁()),F₃()] in g \/ {[(EmptyIns F₁()),F₃()]} by XBOOLE_0:def 3;
then [(EmptyIns F₁()),F₃()] in (g \/ {[(EmptyIns F₁()),F₃()]}) \/ H₁(i,g) by XBOOLE_0:def 3;
then [(EmptyIns F₁()),F₃()] in ((g \/ {[(EmptyIns F₁()),F₃()]}) \/ H₁(i,g)) \/ H₂(i,g) by XBOOLE_0:def 3;
then [(EmptyIns F₁()),F₃()] in h by A24, XBOOLE_0:def 3;
hence h . (EmptyIns F₁()) = F₃() by FUNCT_1:1; :: thesis: verum

end;

hereby :: thesis: ( ( for C, I1, I2 being Element of F₁() st if-then-else (C,I1,I2) in (ElementaryInstructions F₁()) |^ (i + 1) holds
h . (if-then-else (C,I1,I2)) = F₇((h . C),(h . I1),(h . I2)) ) & ( for C, I being Element of F₁() st while (C,I) in (ElementaryInstructions F₁()) |^ (i + 1) holds
h . (while (C,I)) = F₆((h . C),(h . I)) ) )

let I1, I2 be Element of F₁(); :: thesis: ( I1 \; I2 in (ElementaryInstructions F₁()) |^ (i + 1) implies h . (I1 \; I2) = F₅((h . I1),(h . I2)) )
set x = I1 \; I2;
set y = F₅((h . I1),(h . I2));
assume I1 \; I2 in (ElementaryInstructions F₁()) |^ (i + 1) ; :: thesis: h . (I1 \; I2) = F₅((h . I1),(h . I2))
then A152: ex i0 being Nat st
( i + 1 = i0 + 1 & I1 in (ElementaryInstructions F₁()) |^ i0 & I2 in (ElementaryInstructions F₁()) |^ i0 ) by Th88;
then reconsider gI1 = g . I1, gI2 = g . I2 as Element of F₂() by FUNCT_2:5;
A153: [I1,gI1] in g by A25, A152, FUNCT_1:def 2;
A154: [I2,gI2] in g by A25, A152, FUNCT_1:def 2;
A155: g . I1 = h . I1 by A151, A153, FUNCT_1:1;
g . I2 = h . I2 by A151, A154, FUNCT_1:1;
then [(I1 \; I2),F₅((h . I1),(h . I2))] in H₁(i,g) by A152, A153, A154, A155;
then [(I1 \; I2),F₅((h . I1),(h . I2))] in (g \/ {[(EmptyIns F₁()),F₃()]}) \/ H₁(i,g) by XBOOLE_0:def 3;
then [(I1 \; I2),F₅((h . I1),(h . I2))] in ((g \/ {[(EmptyIns F₁()),F₃()]}) \/ H₁(i,g)) \/ H₂(i,g) by XBOOLE_0:def 3;
then [(I1 \; I2),F₅((h . I1),(h . I2))] in h by A24, XBOOLE_0:def 3;
hence h . (I1 \; I2) = F₅((h . I1),(h . I2)) by FUNCT_1:1; :: thesis: verum

end;

hereby :: thesis: for C, I being Element of F₁() st while (C,I) in (ElementaryInstructions F₁()) |^ (i + 1) holds
h . (while (C,I)) = F₆((h . C),(h . I))

let C, I1, I2 be Element of F₁(); :: thesis: ( if-then-else (C,I1,I2) in (ElementaryInstructions F₁()) |^ (i + 1) implies h . (if-then-else (C,I1,I2)) = F₇((h . C),(h . I1),(h . I2)) )
set x = if-then-else (C,I1,I2);
set y = F₇((h . C),(h . I1),(h . I2));
assume if-then-else (C,I1,I2) in (ElementaryInstructions F₁()) |^ (i + 1) ; :: thesis: h . (if-then-else (C,I1,I2)) = F₇((h . C),(h . I1),(h . I2))
then A156: ex i0 being Nat st
( i + 1 = i0 + 1 & C in (ElementaryInstructions F₁()) |^ i0 & I1 in (ElementaryInstructions F₁()) |^ i0 & I2 in (ElementaryInstructions F₁()) |^ i0 ) by Th89;
then reconsider gC = g . C, gI1 = g . I1, gI2 = g . I2 as Element of F₂() by FUNCT_2:5;
A157: [C,gC] in g by A25, A156, FUNCT_1:def 2;
A158: [I1,gI1] in g by A25, A156, FUNCT_1:def 2;
A159: [I2,gI2] in g by A25, A156, FUNCT_1:def 2;
A160: g . C = h . C by A151, A157, FUNCT_1:1;
A161: g . I1 = h . I1 by A151, A158, FUNCT_1:1;
g . I2 = h . I2 by A151, A159, FUNCT_1:1;
then [(if-then-else (C,I1,I2)),F₇((h . C),(h . I1),(h . I2))] in H₂(i,g) by A156, A157, A158, A159, A160, A161;
then [(if-then-else (C,I1,I2)),F₇((h . C),(h . I1),(h . I2))] in ((g \/ {[(EmptyIns F₁()),F₃()]}) \/ H₁(i,g)) \/ H₂(i,g) by XBOOLE_0:def 3;
then [(if-then-else (C,I1,I2)),F₇((h . C),(h . I1),(h . I2))] in h by A24, XBOOLE_0:def 3;
hence h . (if-then-else (C,I1,I2)) = F₇((h . C),(h . I1),(h . I2)) by FUNCT_1:1; :: thesis: verum

end;

let C, I be Element of F₁(); :: thesis: ( while (C,I) in (ElementaryInstructions F₁()) |^ (i + 1) implies h . (while (C,I)) = F₆((h . C),(h . I)) )
set x = while (C,I);
set y = F₆((h . C),(h . I));
assume while (C,I) in (ElementaryInstructions F₁()) |^ (i + 1) ; :: thesis: h . (while (C,I)) = F₆((h . C),(h . I))
then A162: ex i0 being Nat st
( i + 1 = i0 + 1 & C in (ElementaryInstructions F₁()) |^ i0 & I in (ElementaryInstructions F₁()) |^ i0 ) by Th90;
then reconsider gC = g . C, gI = g . I as Element of F₂() by FUNCT_2:5;
A163: [C,gC] in g by A25, A162, FUNCT_1:def 2;
A164: [I,gI] in g by A25, A162, FUNCT_1:def 2;
A165: g . C = h . C by A151, A163, FUNCT_1:1;
g . I = h . I by A151, A164, FUNCT_1:1;
then [(while (C,I)),F₆((h . C),(h . I))] in H₃(i,g) by A162, A163, A164, A165;
then [(while (C,I)),F₆((h . C),(h . I))] in h by A24, XBOOLE_0:def 3;
hence h . (while (C,I)) = F₆((h . C),(h . I)) by FUNCT_1:1; :: thesis: verum

end;

A166: for i being Nat holds S₁[i] from NAT_1:sch 2(A15, A17);
( Union FF is Relation-like & Union FF is Function-like )

proof

hereby :: according to RELAT_1:def 1 :: thesis: Union FF is Function-like

let x be object ; :: thesis: ( x in Union FF implies ex a, b being object st x = [a,b] )
assume x in Union FF ; :: thesis: ex a, b being object st x = [a,b]
then consider n being object such that
A167: n in dom FF and
A168: x in FF . n by CARD_5:2;
reconsider n = n as Element of NAT by A3, A167;
S₁[n] by A166;
hence ex a, b being object st x = [a,b] by A168, RELAT_1:def 1; :: thesis: verum

end;

let x, y1, y2 be object ; :: according to FUNCT_1:def 1 :: thesis: ( [x,y1] nin Union FF or [x,y2] nin Union FF or y1 = y2 )
assume [x,y1] in Union FF ; :: thesis: ( [x,y2] nin Union FF or y1 = y2 )
then consider n1 being object such that
A169: n1 in dom FF and
A170: [x,y1] in FF . n1 by CARD_5:2;
assume [x,y2] in Union FF ; :: thesis: y1 = y2
then consider n2 being object such that
A171: n2 in dom FF and
A172: [x,y2] in FF . n2 by CARD_5:2;
reconsider n1 = n1, n2 = n2 as Element of NAT by A3, A169, A171;
( n1 <= n2 or n2 <= n1 ) ;
then ( FF . n1 c= FF . n2 or FF . n2 c= FF . n1 ) by A5;
then ( ( [x,y1] in FF . n2 & S₁[n2] ) or ( [x,y2] in FF . n1 & S₁[n1] ) ) by A166, A170, A172;
hence y1 = y2 by A170, A172, FUNCT_1:def 1; :: thesis: verum

end;

then reconsider f = Union FF as Function ;
A173: dom f = the carrier of F₁()

proof

thus dom f c= the carrier of F₁() :: according to XBOOLE_0:def 10 :: thesis: the carrier of F₁() c= dom f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( x nin dom f or not x nin the carrier of F₁() )
assume x in dom f ; :: thesis: not x nin the carrier of F₁()
then [x,(f . x)] in f by FUNCT_1:def 2;
then consider n being object such that
A174: n in dom FF and
A175: [x,(f . x)] in FF . n by CARD_5:2;
reconsider n = n as Element of NAT by A3, A174;
S₁[n] by A166;
then x in (ElementaryInstructions F₁()) |^ n by A175, ZFMISC_1:87;
hence not x nin the carrier of F₁() ; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( x nin the carrier of F₁() or not x nin dom f )
assume x in the carrier of F₁() ; :: thesis: not x nin dom f
then reconsider I = x as Element of F₁() ;
consider n being Nat such that
A176: I in (ElementaryInstructions F₁()) |^ n by Th79;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
S₁[n] by A166;
then reconsider g = FF . n as Function of ((ElementaryInstructions F₁()) |^ n),F₂() ;
dom g = (ElementaryInstructions F₁()) |^ n by FUNCT_2:def 1;
then [I,(g . I)] in g by A176, FUNCT_1:def 2;
then [I,(g . I)] in f by A3, CARD_5:2;
hence not x nin dom f by XTUPLE_0:def 12; :: thesis: verum

end;

rng f c= F₂()

proof

let b be object ; :: according to TARSKI:def 3 :: thesis: ( b nin rng f or not b nin F₂() )
assume b in rng f ; :: thesis: not b nin F₂()
then consider a being object such that
A177: a in dom f and
A178: b = f . a by FUNCT_1:def 3;
reconsider a = a as Element of F₁() by A173, A177;
consider n being Nat such that
A179: a in (ElementaryInstructions F₁()) |^ n by Th79;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
S₁[n] by A166;
then reconsider g = FF . n as Function of ((ElementaryInstructions F₁()) |^ n),F₂() ;
A180: dom g = (ElementaryInstructions F₁()) |^ n by FUNCT_2:def 1;
then [a,(g . a)] in g by A179, FUNCT_1:def 2;
then [a,(g . a)] in f by A3, CARD_5:2;
then A181: b = g . a by A178, FUNCT_1:1;
g . a in rng g by A179, A180, FUNCT_1:3;
hence not b nin F₂() by A181; :: thesis: verum

end;

then reconsider f = f as Function of the carrier of F₁(),F₂() by A173, FUNCT_2:2;
take f ; :: thesis: ( ( for I being Element of F₁() st I in ElementaryInstructions F₁() holds
f . I = F₄(I) ) & f . (EmptyIns F₁()) = F₃() & ( for I1, I2 being Element of F₁() holds f . (I1 \; I2) = F₅((f . I1),(f . I2)) ) & ( for C, I1, I2 being Element of F₁() holds f . (if-then-else (C,I1,I2)) = F₇((f . C),(f . I1),(f . I2)) ) & ( for C, I being Element of F₁() holds f . (while (C,I)) = F₆((f . C),(f . I)) ) )

hereby :: thesis: ( f . (EmptyIns F₁()) = F₃() & ( for I1, I2 being Element of F₁() holds f . (I1 \; I2) = F₅((f . I1),(f . I2)) ) & ( for C, I1, I2 being Element of F₁() holds f . (if-then-else (C,I1,I2)) = F₇((f . C),(f . I1),(f . I2)) ) & ( for C, I being Element of F₁() holds f . (while (C,I)) = F₆((f . C),(f . I)) ) )

let I be Element of F₁(); :: thesis: ( I in ElementaryInstructions F₁() implies f . I = F₄(I) )
assume I in ElementaryInstructions F₁() ; :: thesis: f . I = F₄(I)
then [I,F₄(I)] in FF . 0 by A3;
then [I,F₄(I)] in f by A3, CARD_5:2;
hence f . I = F₄(I) by FUNCT_1:1; :: thesis: verum

end;

A182: now :: thesis: for n being Nat
for I being Element of F₁()
for g being Function of ((ElementaryInstructions F₁()) |^ n),F₂() st I in (ElementaryInstructions F₁()) |^ n & g = FF . n holds
g . I = f . I

let n be Nat; :: thesis: for I being Element of F₁()
for g being Function of ((ElementaryInstructions F₁()) |^ n),F₂() st I in (ElementaryInstructions F₁()) |^ n & g = FF . n holds
g . I = f . I
let I be Element of F₁(); :: thesis: for g being Function of ((ElementaryInstructions F₁()) |^ n),F₂() st I in (ElementaryInstructions F₁()) |^ n & g = FF . n holds
g . I = f . I
let g be Function of ((ElementaryInstructions F₁()) |^ n),F₂(); :: thesis: ( I in (ElementaryInstructions F₁()) |^ n & g = FF . n implies g . I = f . I )
assume that
A183: I in (ElementaryInstructions F₁()) |^ n and
A184: g = FF . n ; :: thesis: g . I = f . I
dom g = (ElementaryInstructions F₁()) |^ n by FUNCT_2:def 1;
then A185: [I,(g . I)] in g by A183, FUNCT_1:def 2;
n in NAT by ORDINAL1:def 12;
then [I,(g . I)] in f by A3, A184, A185, CARD_5:2;
hence g . I = f . I by FUNCT_1:1; :: thesis: verum

end;

consider n0 being Nat such that
A186: EmptyIns F₁() in (ElementaryInstructions F₁()) |^ n0 by Th79;
reconsider n0 = n0 as Element of NAT by ORDINAL1:def 12;
consider g0 being Function of ((ElementaryInstructions F₁()) |^ n0),F₂() such that
A187: g0 = FF . n0 and
A188: ( EmptyIns F₁() in (ElementaryInstructions F₁()) |^ n0 implies g0 . (EmptyIns F₁()) = F₃() ) and
for I1, I2 being Element of F₁() st I1 \; I2 in (ElementaryInstructions F₁()) |^ n0 holds
g0 . (I1 \; I2) = F₅((g0 . I1),(g0 . I2)) and
for C, I1, I2 being Element of F₁() st if-then-else (C,I1,I2) in (ElementaryInstructions F₁()) |^ n0 holds
g0 . (if-then-else (C,I1,I2)) = F₇((g0 . C),(g0 . I1),(g0 . I2)) and
for C, I being Element of F₁() st while (C,I) in (ElementaryInstructions F₁()) |^ n0 holds
g0 . (while (C,I)) = F₆((g0 . C),(g0 . I)) by A166;
dom g0 = (ElementaryInstructions F₁()) |^ n0 by FUNCT_2:def 1;
then [(EmptyIns F₁()),F₃()] in g0 by A186, A188, FUNCT_1:def 2;
then [(EmptyIns F₁()),F₃()] in f by A3, A187, CARD_5:2;
hence f . (EmptyIns F₁()) = F₃() by FUNCT_1:1; :: thesis: ( ( for I1, I2 being Element of F₁() holds f . (I1 \; I2) = F₅((f . I1),(f . I2)) ) & ( for C, I1, I2 being Element of F₁() holds f . (if-then-else (C,I1,I2)) = F₇((f . C),(f . I1),(f . I2)) ) & ( for C, I being Element of F₁() holds f . (while (C,I)) = F₆((f . C),(f . I)) ) )

hereby :: thesis: ( ( for C, I1, I2 being Element of F₁() holds f . (if-then-else (C,I1,I2)) = F₇((f . C),(f . I1),(f . I2)) ) & ( for C, I being Element of F₁() holds f . (while (C,I)) = F₆((f . C),(f . I)) ) )

let I1, I2 be Element of F₁(); :: thesis: f . (I1 \; I2) = F₅((f . I1),(f . I2))
consider n0 being Nat such that
A189: I1 \; I2 in (ElementaryInstructions F₁()) |^ n0 by Th79;
reconsider n0 = n0 as Element of NAT by ORDINAL1:def 12;
consider g0 being Function of ((ElementaryInstructions F₁()) |^ n0),F₂() such that
A190: g0 = FF . n0 and
( EmptyIns F₁() in (ElementaryInstructions F₁()) |^ n0 implies g0 . (EmptyIns F₁()) = F₃() ) and
A191: for I1, I2 being Element of F₁() st I1 \; I2 in (ElementaryInstructions F₁()) |^ n0 holds
g0 . (I1 \; I2) = F₅((g0 . I1),(g0 . I2)) and
for C, I1, I2 being Element of F₁() st if-then-else (C,I1,I2) in (ElementaryInstructions F₁()) |^ n0 holds
g0 . (if-then-else (C,I1,I2)) = F₇((g0 . C),(g0 . I1),(g0 . I2)) and
for C, I being Element of F₁() st while (C,I) in (ElementaryInstructions F₁()) |^ n0 holds
g0 . (while (C,I)) = F₆((g0 . C),(g0 . I)) by A166;
consider i0 being Nat such that
A192: n0 = i0 + 1 and
A193: I1 in (ElementaryInstructions F₁()) |^ i0 and
A194: I2 in (ElementaryInstructions F₁()) |^ i0 by A189, Th88;
n0 > i0 by A192, NAT_1:13;
then A195: (ElementaryInstructions F₁()) |^ i0 c= (ElementaryInstructions F₁()) |^ n0 by Th21;
A196: dom g0 = (ElementaryInstructions F₁()) |^ n0 by FUNCT_2:def 1;
A197: g0 . I1 = f . I1 by A182, A190, A193, A195;
A198: g0 . I2 = f . I2 by A182, A190, A194, A195;
A199: [(I1 \; I2),(g0 . (I1 \; I2))] in g0 by A189, A196, FUNCT_1:1;
g0 . (I1 \; I2) = F₅((f . I1),(f . I2)) by A189, A191, A197, A198;
then [(I1 \; I2),F₅((f . I1),(f . I2))] in f by A3, A190, A199, CARD_5:2;
hence f . (I1 \; I2) = F₅((f . I1),(f . I2)) by FUNCT_1:1; :: thesis: verum

end;

hereby :: thesis: for C, I being Element of F₁() holds f . (while (C,I)) = F₆((f . C),(f . I))

let C, I1, I2 be Element of F₁(); :: thesis: f . (if-then-else (C,I1,I2)) = F₇((f . C),(f . I1),(f . I2))
set IF = if-then-else (C,I1,I2);
consider n0 being Nat such that
A200: if-then-else (C,I1,I2) in (ElementaryInstructions F₁()) |^ n0 by Th79;
reconsider n0 = n0 as Element of NAT by ORDINAL1:def 12;
consider g0 being Function of ((ElementaryInstructions F₁()) |^ n0),F₂() such that
A201: g0 = FF . n0 and
( EmptyIns F₁() in (ElementaryInstructions F₁()) |^ n0 implies g0 . (EmptyIns F₁()) = F₃() ) and
for I1, I2 being Element of F₁() st I1 \; I2 in (ElementaryInstructions F₁()) |^ n0 holds
g0 . (I1 \; I2) = F₅((g0 . I1),(g0 . I2)) and
A202: for C, I1, I2 being Element of F₁() st if-then-else (C,I1,I2) in (ElementaryInstructions F₁()) |^ n0 holds
g0 . (if-then-else (C,I1,I2)) = F₇((g0 . C),(g0 . I1),(g0 . I2)) and
for C, I being Element of F₁() st while (C,I) in (ElementaryInstructions F₁()) |^ n0 holds
g0 . (while (C,I)) = F₆((g0 . C),(g0 . I)) by A166;
consider i0 being Nat such that
A203: n0 = i0 + 1 and
A204: C in (ElementaryInstructions F₁()) |^ i0 and
A205: I1 in (ElementaryInstructions F₁()) |^ i0 and
A206: I2 in (ElementaryInstructions F₁()) |^ i0 by A200, Th89;
n0 > i0 by A203, NAT_1:13;
then A207: (ElementaryInstructions F₁()) |^ i0 c= (ElementaryInstructions F₁()) |^ n0 by Th21;
A208: dom g0 = (ElementaryInstructions F₁()) |^ n0 by FUNCT_2:def 1;
A209: g0 . C = f . C by A182, A201, A204, A207;
A210: g0 . I1 = f . I1 by A182, A201, A205, A207;
A211: g0 . I2 = f . I2 by A182, A201, A206, A207;
A212: [(if-then-else (C,I1,I2)),(g0 . (if-then-else (C,I1,I2)))] in g0 by A200, A208, FUNCT_1:1;
g0 . (if-then-else (C,I1,I2)) = F₇((f . C),(f . I1),(f . I2)) by A200, A202, A209, A210, A211;
then [(if-then-else (C,I1,I2)),F₇((f . C),(f . I1),(f . I2))] in f by A3, A201, A212, CARD_5:2;
hence f . (if-then-else (C,I1,I2)) = F₇((f . C),(f . I1),(f . I2)) by FUNCT_1:1; :: thesis: verum

end;

let C, I be Element of F₁(); :: thesis: f . (while (C,I)) = F₆((f . C),(f . I))
set WH = while (C,I);
consider n0 being Nat such that
A213: while (C,I) in (ElementaryInstructions F₁()) |^ n0 by Th79;
reconsider n0 = n0 as Element of NAT by ORDINAL1:def 12;
consider g0 being Function of ((ElementaryInstructions F₁()) |^ n0),F₂() such that
A214: g0 = FF . n0 and
( EmptyIns F₁() in (ElementaryInstructions F₁()) |^ n0 implies g0 . (EmptyIns F₁()) = F₃() ) and
for I1, I2 being Element of F₁() st I1 \; I2 in (ElementaryInstructions F₁()) |^ n0 holds
g0 . (I1 \; I2) = F₅((g0 . I1),(g0 . I2)) and
for C, I1, I2 being Element of F₁() st if-then-else (C,I1,I2) in (ElementaryInstructions F₁()) |^ n0 holds
g0 . (if-then-else (C,I1,I2)) = F₇((g0 . C),(g0 . I1),(g0 . I2)) and
A215: for C, I being Element of F₁() st while (C,I) in (ElementaryInstructions F₁()) |^ n0 holds
g0 . (while (C,I)) = F₆((g0 . C),(g0 . I)) by A166;
consider i0 being Nat such that
A216: n0 = i0 + 1 and
A217: C in (ElementaryInstructions F₁()) |^ i0 and
A218: I in (ElementaryInstructions F₁()) |^ i0 by A213, Th90;
n0 > i0 by A216, NAT_1:13;
then A219: (ElementaryInstructions F₁()) |^ i0 c= (ElementaryInstructions F₁()) |^ n0 by Th21;
A220: dom g0 = (ElementaryInstructions F₁()) |^ n0 by FUNCT_2:def 1;
A221: g0 . C = f . C by A182, A214, A217, A219;
A222: g0 . I = f . I by A182, A214, A218, A219;
A223: [(while (C,I)),(g0 . (while (C,I)))] in g0 by A213, A220, FUNCT_1:1;
g0 . (while (C,I)) = F₆((f . C),(f . I)) by A213, A215, A221, A222;
then [(while (C,I)),F₆((f . C),(f . I))] in f by A3, A214, A223, CARD_5:2;
hence f . (while (C,I)) = F₆((f . C),(f . I)) by FUNCT_1:1; :: thesis: verum