let f1, f2 be non empty NAT * -defined to-naturals homogeneous Function; :: thesis:
let p be Element of ((arity f1) + 1) -tuples_on NAT; :: thesis:
let i, m be Nat; :: thesis:
set p0 = p +* (i,0);
consider G being Function of (((arity f1) + 1) -tuples_on NAT),(HFuncs NAT) such that
A1: primrec (f1,f2,i) = Union G and
A2: for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec (f1,f2,i,p) by Def11;
reconsider rngG = rng G as functional compatible set by A1, Th10;
assume A3: i in dom p ; :: thesis:

let k be Element of NAT ; :: thesis:
assume that
A5: p +* (i,k) in dom (primrec (f1,f2,i)) and
A6: not p +* (i,k) in dom (G . (p +* (i,k))) ; :: thesis:
union rngG <> {} by A1, A5;
then reconsider rngG = rng G as non empty functional compatible set ;
set pk = p +* (i,k);
dom (union rngG) = union { (dom f) where f is Element of rngG : verum } by Th11;
then consider X being set such that
A7: p +* (i,k) in X and
A8: X in { (dom f) where f is Element of rngG : verum } by A1, A5, TARSKI:def 4;
consider f being Element of rngG such that
A9: X = dom f by A8;
consider pp being object such that
A10: pp in dom G and
A11: f = G . pp by FUNCT_1:def 3;
reconsider pp = pp as Element of ((arity f1) + 1) -tuples_on NAT by A10;
G . pp = primrec (f1,f2,i,pp) by A2;
then A12: ex m being Element of NAT st p +* (i,k) = pp +* (i,m) by A7, A9, A11, Th48;
set ppi = pp . i;
A13: p +* (i,(pp . i)) = (p +* (i,k)) +* (i,(pp . i)) by FUNCT_7:34
.= pp +* (i,(pp . i)) by A12, FUNCT_7:34
.= pp by FUNCT_7:35 ;

suppose k = pp . i ; :: thesis:

hence contradiction by A6, A7, A9, A11, A13; :: thesis:

end;

suppose pp . i < k ; :: thesis:

then consider m being Nat such that
A14: k = (pp . i) + m by NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
k = (pp . i) + m by A14;
then dom (G . pp) c= dom (G . (p +* (i,k))) by A3, A2, A13, Lm4;
hence contradiction by A6, A7, A9, A11; :: thesis:

end;

suppose pp . i > k ; :: thesis:

then consider m being Nat such that
A15: pp . i = k + m by NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
pp . i = k + m by A15;
hence contradiction by A3, A2, A6, A7, A9, A11, A13, Lm5; :: thesis:

end;

A16: dom p = dom (p +* (i,0)) by FUNCT_7:30;

A17: now :: thesis:

A18: p +* (i,0) in {(p +* (i,0))} by TARSKI:def 1;
A19: (p +* (i,0)) /. i = (p +* (i,0)) . i by A3, A16, PARTFUN1:def 6
.= 0 by A3, FUNCT_7:31 ;
consider F being sequence of (HFuncs NAT) such that
A20: primrec (f1,f2,i,(p +* (i,0))) = F . ((p +* (i,0)) /. i) and
A21: ( i in dom (p +* (i,0)) & Del ((p +* (i,0)),i) in dom f1 implies F . 0 = ((p +* (i,0)) +* (i,0)) .--> (f1 . (Del ((p +* (i,0)),i))) ) and
A22: ( ( not i in dom (p +* (i,0)) or not Del ((p +* (i,0)),i) in dom f1 ) implies F . 0 = {} ) and
for m being Nat holds S₁[m,F . m,F . (m + 1),p +* (i,0),i,f2] by Def10;
A23: G . (p +* (i,0)) = primrec (f1,f2,i,(p +* (i,0))) by A2;
thus ( p +* (i,0) in dom (G . (p +* (i,0))) iff Del (p,i) in dom f1 ) :: thesis:

proof

thus ( p +* (i,0) in dom (G . (p +* (i,0))) implies Del (p,i) in dom f1 ) by A2, A20, A22, A19, Th3; :: thesis:
assume Del (p,i) in dom f1 ; :: thesis:
then dom (F . 0) = {(p +* (i,0))} by A3, A21, Th3, FUNCT_7:30, FUNCT_7:34;
hence p +* (i,0) in dom (G . (p +* (i,0))) by A23, A20, A19, TARSKI:def 1; :: thesis:

end;

assume p +* (i,0) in dom (G . (p +* (i,0))) ; :: thesis:
then F . 0 = {(p +* (i,0))} --> (f1 . (Del ((p +* (i,0)),i))) by A2, A20, A21, A22, A19, FUNCT_7:34;
then F . 0 = {(p +* (i,0))} --> (f1 . (Del (p,i))) by Th3;
hence (G . (p +* (i,0))) . (p +* (i,0)) = f1 . (Del (p,i)) by A23, A20, A19, A18, FUNCOP_1:7; :: thesis:

end;

reconsider mm = m as Element of NAT by ORDINAL1:def 12;
set pm1 = p +* (i,(mm + 1));
set pm = p +* (i,mm);
set pc = <*((G . (p +* (i,(mm + 1)))) . ((p +* (i,(mm + 1))) +* (i,m)))*>;
A24: dom G = ((arity f1) + 1) -tuples_on NAT by FUNCT_2:def 1;
then A25: G . (p +* (i,(mm + 1))) in rng G by FUNCT_1:def 3;
reconsider rngG = rngG as non empty functional compatible set ;
A26: G . (p +* (i,0)) in rng G by A24, FUNCT_1:def 3;
thus ( p +* (i,0) in dom (primrec (f1,f2,i)) iff Del (p,i) in dom f1 ) :: thesis:

proof

thus ( p +* (i,0) in dom (primrec (f1,f2,i)) implies Del (p,i) in dom f1 ) by A4, A17; :: thesis:
assume A27: Del (p,i) in dom f1 ; :: thesis:
dom (G . (p +* (i,0))) in { (dom f) where f is Element of rngG : verum } by A26;
then p +* (i,0) in union { (dom f) where f is Element of rngG : verum } by A17, A27, TARSKI:def 4;
hence p +* (i,0) in dom (primrec (f1,f2,i)) by A1, Th11; :: thesis:

end;

hereby :: thesis:

assume A28: p +* (i,0) in dom (primrec (f1,f2,i)) ; :: thesis:
then p +* (i,0) in dom (G . (p +* (i,0))) by A4;
then (union rngG) . (p +* (i,0)) = (G . (p +* (i,0))) . (p +* (i,0)) by A26, Th12;
hence (primrec (f1,f2,i)) . (p +* (i,0)) = f1 . (Del (p,i)) by A1, A4, A17, A28; :: thesis:

end;

A29: dom p = dom (p +* (i,(mm + 1))) by FUNCT_7:30;
A30: (p +* (i,(mm + 1))) +* (i,(m + 1)) = p +* (i,(mm + 1)) by FUNCT_7:34;
A31: (p +* (i,(mm + 1))) +* (i,m) = p +* (i,mm) by FUNCT_7:34;
A32: dom p = dom (p +* (i,mm)) by FUNCT_7:30;

A33: now :: thesis:

A34: (p +* (i,mm)) /. i = (p +* (i,mm)) . i by A3, A32, PARTFUN1:def 6
.= m by A3, FUNCT_7:31 ;
consider F being sequence of (HFuncs NAT) such that
A35: primrec (f1,f2,i,(p +* (i,mm))) = F . ((p +* (i,mm)) /. i) and
A36: ( i in dom (p +* (i,mm)) & Del ((p +* (i,mm)),i) in dom f1 implies F . 0 = ((p +* (i,mm)) +* (i,0)) .--> (f1 . (Del ((p +* (i,mm)),i))) ) and
A37: ( ( not i in dom (p +* (i,mm)) or not Del ((p +* (i,mm)),i) in dom f1 ) implies F . 0 = {} ) and
A38: for M being Nat holds S₁[M,F . M,F . (M + 1),p +* (i,mm),i,f2] by Def10;
A39: G . (p +* (i,(mm + 1))) = primrec (f1,f2,i,(p +* (i,(mm + 1)))) by A2;
consider F1 being sequence of (HFuncs NAT) such that
A40: primrec (f1,f2,i,(p +* (i,(mm + 1)))) = F1 . ((p +* (i,(mm + 1))) /. i) and
A41: ( i in dom (p +* (i,(mm + 1))) & Del ((p +* (i,(mm + 1))),i) in dom f1 implies F1 . 0 = ((p +* (i,(mm + 1))) +* (i,0)) .--> (f1 . (Del ((p +* (i,(mm + 1))),i))) ) and
A42: ( ( not i in dom (p +* (i,(mm + 1))) or not Del ((p +* (i,(mm + 1))),i) in dom f1 ) implies F1 . 0 = {} ) and
A43: for M being Nat holds S₁[M,F1 . M,F1 . (M + 1),p +* (i,(mm + 1)),i,f2] by Def10;
A44: (F1 . (m + 1)) . (p +* (i,mm)) = (F1 . m) . (p +* (i,mm)) by A3, A41, A42, A43, Lm3;
A45: p +* (i,(mm + 1)) in {(p +* (i,(mm + 1)))} by TARSKI:def 1;
then A46: p +* (i,(mm + 1)) in dom ({(p +* (i,(mm + 1)))} --> (f2 . ((p +* (i,mm)) ^ <*((F1 . m) . (p +* (i,mm)))*>))) ;
A47: G . (p +* (i,mm)) = primrec (f1,f2,i,(p +* (i,mm))) by A2;
A48: (p +* (i,(mm + 1))) /. i = (p +* (i,(mm + 1))) . i by A3, A29, PARTFUN1:def 6
.= m + 1 by A3, FUNCT_7:31 ;
A49: F1 . m = F . m by A41, A42, A43, A36, A37, A38, Lm2;
A50: not p +* (i,(mm + 1)) in dom (F1 . m) by A3, A41, A42, A43, Lm3;
thus A51: ( p +* (i,(mm + 1)) in dom (G . (p +* (i,(mm + 1)))) iff ( p +* (i,mm) in dom (G . (p +* (i,mm))) & (p +* (i,mm)) ^ <*((G . (p +* (i,(mm + 1)))) . ((p +* (i,(mm + 1))) +* (i,m)))*> in dom f2 ) ) :: thesis:

proof

hereby :: thesis:

assume A52: p +* (i,(mm + 1)) in dom (G . (p +* (i,(mm + 1)))) ; :: thesis:
then A53: p +* (i,(mm + 1)) in dom (F1 . (m + 1)) by A2, A40, A48;
assume A54: ( not p +* (i,mm) in dom (G . (p +* (i,mm))) or not (p +* (i,mm)) ^ <*((G . (p +* (i,(mm + 1)))) . ((p +* (i,(mm + 1))) +* (i,m)))*> in dom f2 ) ; :: thesis:

per cases by A54;

suppose not p +* (i,mm) in dom (G . (p +* (i,mm))) ; :: thesis:

then not p +* (i,mm) in dom (F1 . m) by A2, A35, A34, A49;
hence contradiction by A31, A43, A50, A53; :: thesis:

end;

suppose not (p +* (i,mm)) ^ <*((G . (p +* (i,(mm + 1)))) . ((p +* (i,(mm + 1))) +* (i,m)))*> in dom f2 ; :: thesis:

hence contradiction by A31, A39, A40, A43, A48, A44, A50, A52; :: thesis:

end;

assume that
A55: p +* (i,mm) in dom (G . (p +* (i,mm))) and
A56: (p +* (i,mm)) ^ <*((G . (p +* (i,(mm + 1)))) . ((p +* (i,(mm + 1))) +* (i,m)))*> in dom f2 ; :: thesis:
p +* (i,(mm + 1)) in {(p +* (i,(mm + 1)))} by TARSKI:def 1;
then p +* (i,(mm + 1)) in dom ({(p +* (i,(mm + 1)))} --> (f2 . ((p +* (i,mm)) ^ <*((F1 . m) . (p +* (i,mm)))*>))) ;
then A57: p +* (i,(mm + 1)) in (dom (F1 . m)) \/ (dom ({(p +* (i,(mm + 1)))} --> (f2 . ((p +* (i,mm)) ^ <*((F1 . m) . (p +* (i,mm)))*>)))) by XBOOLE_0:def 3;
F1 . (m + 1) = (F1 . m) +* ((p +* (i,(mm + 1))) .--> (f2 . ((p +* (i,mm)) ^ <*((F1 . m) . (p +* (i,mm)))*>))) by A3, A29, A31, A30, A39, A47, A40, A43, A35, A48, A34, A49, A44, A55, A56;
hence p +* (i,(mm + 1)) in dom (G . (p +* (i,(mm + 1)))) by A39, A40, A48, A57, FUNCT_4:def 1; :: thesis:

end;

assume A58: p +* (i,(mm + 1)) in dom (G . (p +* (i,(mm + 1)))) ; :: thesis:
then (p +* (i,mm)) ^ <*((F1 . m) . (p +* (i,mm)))*> in dom f2 by A31, A39, A40, A43, A48, A51;
then F1 . (m + 1) = (F1 . m) +* ((p +* (i,(mm + 1))) .--> (f2 . ((p +* (i,mm)) ^ <*((F1 . m) . (p +* (i,mm)))*>))) by A3, A29, A31, A30, A47, A43, A35, A34, A49, A51, A58;
hence (G . (p +* (i,(mm + 1)))) . (p +* (i,(mm + 1))) = ({(p +* (i,(mm + 1)))} --> (f2 . ((p +* (i,mm)) ^ <*((F1 . m) . (p +* (i,mm)))*>))) . (p +* (i,(mm + 1))) by A39, A40, A48, A46, FUNCT_4:13
.= f2 . ((p +* (i,mm)) ^ <*((G . (p +* (i,(mm + 1)))) . ((p +* (i,(mm + 1))) +* (i,m)))*>) by A31, A39, A40, A48, A44, A45, FUNCOP_1:7 ;
:: thesis:

end;

thus ( p +* (i,(m + 1)) in dom (primrec (f1,f2,i)) iff ( p +* (i,m) in dom (primrec (f1,f2,i)) & (p +* (i,m)) ^ <*((primrec (f1,f2,i)) . (p +* (i,m)))*> in dom f2 ) ) :: thesis:

proof

hereby :: thesis:

assume A59: p +* (i,(m + 1)) in dom (primrec (f1,f2,i)) ; :: thesis:
G . (p +* (i,mm)) in rng G by A24, FUNCT_1:def 3;
then dom (G . (p +* (i,mm))) in { (dom f) where f is Element of rngG : verum } ;
then p +* (i,mm) in union { (dom f) where f is Element of rngG : verum } by A4, A33, A59, TARSKI:def 4;
hence p +* (i,m) in dom (primrec (f1,f2,i)) by A1, Th11; :: thesis:
A60: G . (p +* (i,(mm + 1))) in rng G by A24, FUNCT_1:def 3;
dom (G . (p +* (i,mm))) c= dom (G . (p +* (i,(mm + 1)))) by A3, A2, Lm4;
then (union rngG) . (p +* (i,mm)) = (G . (p +* (i,(mm + 1)))) . (p +* (i,mm)) by A4, A33, A59, A60, Th12;
hence (p +* (i,m)) ^ <*((primrec (f1,f2,i)) . (p +* (i,m)))*> in dom f2 by A1, A4, A33, A59, FUNCT_7:34; :: thesis:

end;

assume that
A61: p +* (i,m) in dom (primrec (f1,f2,i)) and
A62: (p +* (i,m)) ^ <*((primrec (f1,f2,i)) . (p +* (i,m)))*> in dom f2 ; :: thesis:
A63: G . (p +* (i,(mm + 1))) in rng G by A24, FUNCT_1:def 3;
G . (p +* (i,(mm + 1))) in rng G by A24, FUNCT_1:def 3;
then A64: dom (G . (p +* (i,(mm + 1)))) in { (dom f) where f is Element of rngG : verum } ;
A65: dom (G . (p +* (i,mm))) c= dom (G . (p +* (i,(mm + 1)))) by A3, A2, Lm4;
p +* (i,mm) in dom (G . (p +* (i,mm))) by A4, A61;
then p +* (i,(mm + 1)) in union { (dom f) where f is Element of rngG : verum } by A1, A31, A33, A62, A64, A63, A65, Th12, TARSKI:def 4;
hence p +* (i,(m + 1)) in dom (primrec (f1,f2,i)) by A1, Th11; :: thesis:

end;

assume A66: p +* (i,(m + 1)) in dom (primrec (f1,f2,i)) ; :: thesis:
A67: dom (G . (p +* (i,mm))) c= dom (G . (p +* (i,(mm + 1)))) by A3, A2, Lm4;
then A68: (union rngG) . (p +* (i,(mm + 1))) = (G . (p +* (i,(mm + 1)))) . (p +* (i,(mm + 1))) by A4, A66, A25, Th12;
(union rngG) . (p +* (i,mm)) = (G . (p +* (i,(mm + 1)))) . (p +* (i,mm)) by A4, A33, A66, A25, A67, Th12;
hence (primrec (f1,f2,i)) . (p +* (i,(m + 1))) = f2 . ((p +* (i,m)) ^ <*((primrec (f1,f2,i)) . (p +* (i,m)))*>) by A1, A4, A33, A66, A68, FUNCT_7:34; :: thesis: