let i, m be Element of NAT ; :: thesis:
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:
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 Def14;
reconsider rngG = rng G as functional compatible set by A1, Th14;
assume A4: i in dom p ; :: thesis:

A5: now

let k be Element of NAT ; :: thesis:
assume that
A6: p +* (i,k) in dom (primrec (f1,f2,i)) and
A7: not p +* (i,k) in dom (G . (p +* (i,k))) ; :: thesis:
union rngG <> {} by A1, A6;
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 Th15;
then consider X being set such that
A8: p +* (i,k) in X and
A9: X in { (dom f) where f is Element of rngG : verum } by A1, A6, TARSKI:def 4;
consider f being Element of rngG such that
A10: X = dom f and
verum by A9;
consider pp being set such that
A11: pp in dom G and
A12: f = G . pp by FUNCT_1:def 5;
reconsider pp = pp as Element of ((arity f1) + 1) -tuples_on NAT by A11;
G . pp = primrec (f1,f2,i,pp) by A2;
then A13: ex m being Element of NAT st p +* (i,k) = pp +* (i,m) by A8, A10, A12, Th53;
set ppi = pp . i;
A14: p +* (i,(pp . i)) = (p +* (i,k)) +* (i,(pp . i)) by FUNCT_7:36
.= pp +* (i,(pp . i)) by A13, FUNCT_7:36
.= pp by FUNCT_7:37 ;

per cases by XXREAL_0:1;

suppose k = pp . i ; :: thesis:

hence contradiction by A7, A8, A10, A12, A14; :: thesis:

end;

suppose pp . i < k ; :: thesis:

then consider m being Nat such that
A15: k = (pp . i) + m by NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
k = (pp . i) + m by A15;
then dom (G . pp) c= dom (G . (p +* (i,k))) by A4, A2, A14, Lm4;
hence contradiction by A7, A8, A10, A12; :: thesis:

end;

suppose pp . i > k ; :: thesis:

then consider m being Nat such that
A16: pp . i = k + m by NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
pp . i = k + m by A16;
hence contradiction by A4, A2, A7, A8, A10, A12, A14, Lm5; :: thesis:

end;

A17: dom p = dom (p +* (i,0)) by FUNCT_7:32;

A18: now

A19: p +* (i,0) in {(p +* (i,0))} by TARSKI:def 1;
A20: (p +* (i,0)) /. i = (p +* (i,0)) . i by A4, A17, PARTFUN1:def 8
.= 0 by A4, FUNCT_7:33 ;
consider F being Function of NAT,(HFuncs NAT) such that
A21: primrec (f1,f2,i,(p +* (i,0))) = F . ((p +* (i,0)) /. i) and
A22: ( 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
A23: ( ( not i in dom (p +* (i,0)) or not Del ((p +* (i,0)),i) in dom f1 ) implies F . 0 = {} ) and
for m being Element of NAT holds S₁[m,F . m,F . (m + 1),p +* (i,0),i,f2] by Def13;
A24: 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, A21, A23, A20, Th6, RELAT_1:60; :: thesis:
assume Del (p,i) in dom f1 ; :: thesis:
then dom (F . 0) = {((p +* (i,0)) +* (i,0))} by A4, A22, Th6, FUNCOP_1:19, FUNCT_7:32
.= {(p +* (i,0))} by FUNCT_7:36 ;
hence p +* (i,0) in dom (G . (p +* (i,0))) by A24, A21, A20, 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, A21, A22, A23, A20, FUNCT_7:36, RELAT_1:60;
then F . 0 = {(p +* (i,0))} --> (f1 . (Del (p,i))) by Th6;
hence (G . (p +* (i,0))) . (p +* (i,0)) = f1 . (Del (p,i)) by A24, A21, A20, A19, FUNCOP_1:13; :: thesis:

end;

set pm1 = p +* (i,(m + 1));
set pm = p +* (i,m);
set pc = <*((G . (p +* (i,(m + 1)))) . ((p +* (i,(m + 1))) +* (i,m)))*>;
A25: dom G = ((arity f1) + 1) -tuples_on NAT by FUNCT_2:def 1;
then A26: G . (p +* (i,(m + 1))) in rng G by FUNCT_1:def 5;
reconsider rngG = rngG as non empty functional compatible set ;
A27: G . (p +* (i,0)) in rng G by A25, FUNCT_1:def 5;
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 A5, A18; :: thesis:
assume A28: Del (p,i) in dom f1 ; :: thesis:
dom (G . (p +* (i,0))) in { (dom f) where f is Element of rngG : verum } by A27;
then p +* (i,0) in union { (dom f) where f is Element of rngG : verum } by A18, A28, TARSKI:def 4;
hence p +* (i,0) in dom (primrec (f1,f2,i)) by A1, Th15; :: thesis:

end;

hereby :: thesis:

assume A29: p +* (i,0) in dom (primrec (f1,f2,i)) ; :: thesis:
then p +* (i,0) in dom (G . (p +* (i,0))) by A5;
then (union rngG) . (p +* (i,0)) = (G . (p +* (i,0))) . (p +* (i,0)) by A27, Th16;
hence (primrec (f1,f2,i)) . (p +* (i,0)) = f1 . (Del (p,i)) by A1, A5, A18, A29; :: thesis:

end;

A30: dom p = dom (p +* (i,(m + 1))) by FUNCT_7:32;
A31: (p +* (i,(m + 1))) +* (i,(m + 1)) = p +* (i,(m + 1)) by FUNCT_7:36;
A32: (p +* (i,(m + 1))) +* (i,m) = p +* (i,m) by FUNCT_7:36;
A33: dom p = dom (p +* (i,m)) by FUNCT_7:32;

A34: now

A35: (p +* (i,m)) /. i = (p +* (i,m)) . i by A4, A33, PARTFUN1:def 8
.= m by A4, FUNCT_7:33 ;
consider F being Function of NAT,(HFuncs NAT) such that
A36: primrec (f1,f2,i,(p +* (i,m))) = F . ((p +* (i,m)) /. i) and
A37: ( i in dom (p +* (i,m)) & Del ((p +* (i,m)),i) in dom f1 implies F . 0 = ((p +* (i,m)) +* (i,0)) .--> (f1 . (Del ((p +* (i,m)),i))) ) and
A38: ( ( not i in dom (p +* (i,m)) or not Del ((p +* (i,m)),i) in dom f1 ) implies F . 0 = {} ) and
A39: for M being Element of NAT holds S₁[M,F . M,F . (M + 1),p +* (i,m),i,f2] by Def13;
A40: G . (p +* (i,(m + 1))) = primrec (f1,f2,i,(p +* (i,(m + 1)))) by A2;
consider F1 being Function of NAT,(HFuncs NAT) such that
A41: primrec (f1,f2,i,(p +* (i,(m + 1)))) = F1 . ((p +* (i,(m + 1))) /. i) and
A42: ( i in dom (p +* (i,(m + 1))) & Del ((p +* (i,(m + 1))),i) in dom f1 implies F1 . 0 = ((p +* (i,(m + 1))) +* (i,0)) .--> (f1 . (Del ((p +* (i,(m + 1))),i))) ) and
A43: ( ( not i in dom (p +* (i,(m + 1))) or not Del ((p +* (i,(m + 1))),i) in dom f1 ) implies F1 . 0 = {} ) and
A44: for M being Element of NAT holds S₁[M,F1 . M,F1 . (M + 1),p +* (i,(m + 1)),i,f2] by Def13;
A45: (F1 . (m + 1)) . (p +* (i,m)) = (F1 . m) . (p +* (i,m)) by A4, A42, A43, A44, Lm3;
A46: p +* (i,(m + 1)) in {(p +* (i,(m + 1)))} by TARSKI:def 1;
then A47: p +* (i,(m + 1)) in dom ({(p +* (i,(m + 1)))} --> (f2 . ((p +* (i,m)) ^ <*((F1 . m) . (p +* (i,m)))*>))) by FUNCOP_1:19;
A48: G . (p +* (i,m)) = primrec (f1,f2,i,(p +* (i,m))) by A2;
A49: (p +* (i,(m + 1))) /. i = (p +* (i,(m + 1))) . i by A4, A30, PARTFUN1:def 8
.= m + 1 by A4, FUNCT_7:33 ;
A50: F1 . m = F . m by A42, A43, A44, A37, A38, A39, Lm2;
A51: not p +* (i,(m + 1)) in dom (F1 . m) by A4, A42, A43, A44, Lm3;
thus A52: ( p +* (i,(m + 1)) in dom (G . (p +* (i,(m + 1)))) iff ( p +* (i,m) in dom (G . (p +* (i,m))) & (p +* (i,m)) ^ <*((G . (p +* (i,(m + 1)))) . ((p +* (i,(m + 1))) +* (i,m)))*> in dom f2 ) ) :: thesis:

proof

hereby :: thesis:

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

per cases by A55;

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

then not p +* (i,m) in dom (F1 . m) by A2, A36, A35, A50;
hence contradiction by A32, A44, A51, A54; :: thesis:

end;

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

hence contradiction by A32, A40, A41, A44, A49, A45, A51, A53; :: thesis:

end;

assume that
A56: p +* (i,m) in dom (G . (p +* (i,m))) and
A57: (p +* (i,m)) ^ <*((G . (p +* (i,(m + 1)))) . ((p +* (i,(m + 1))) +* (i,m)))*> in dom f2 ; :: thesis:
p +* (i,(m + 1)) in {(p +* (i,(m + 1)))} by TARSKI:def 1;
then p +* (i,(m + 1)) in dom ({(p +* (i,(m + 1)))} --> (f2 . ((p +* (i,m)) ^ <*((F1 . m) . (p +* (i,m)))*>))) by FUNCOP_1:19;
then A58: p +* (i,(m + 1)) in (dom (F1 . m)) \/ (dom ({(p +* (i,(m + 1)))} --> (f2 . ((p +* (i,m)) ^ <*((F1 . m) . (p +* (i,m)))*>)))) by XBOOLE_0:def 3;
F1 . (m + 1) = (F1 . m) +* ((p +* (i,(m + 1))) .--> (f2 . ((p +* (i,m)) ^ <*((F1 . m) . (p +* (i,m)))*>))) by A4, A30, A32, A31, A40, A48, A41, A44, A36, A49, A35, A50, A45, A56, A57;
hence p +* (i,(m + 1)) in dom (G . (p +* (i,(m + 1)))) by A40, A41, A49, A58, FUNCT_4:def 1; :: thesis:

end;

assume A59: p +* (i,(m + 1)) in dom (G . (p +* (i,(m + 1)))) ; :: thesis:
then (p +* (i,m)) ^ <*((F1 . m) . (p +* (i,m)))*> in dom f2 by A32, A40, A41, A44, A49, A52;
then F1 . (m + 1) = (F1 . m) +* ((p +* (i,(m + 1))) .--> (f2 . ((p +* (i,m)) ^ <*((F1 . m) . (p +* (i,m)))*>))) by A4, A30, A32, A31, A48, A44, A36, A35, A50, A52, A59;
hence (G . (p +* (i,(m + 1)))) . (p +* (i,(m + 1))) = ({(p +* (i,(m + 1)))} --> (f2 . ((p +* (i,m)) ^ <*((F1 . m) . (p +* (i,m)))*>))) . (p +* (i,(m + 1))) by A40, A41, A49, A47, FUNCT_4:14
.= f2 . ((p +* (i,m)) ^ <*((G . (p +* (i,(m + 1)))) . ((p +* (i,(m + 1))) +* (i,m)))*>) by A32, A40, A41, A49, A45, A46, FUNCOP_1:13 ;
:: 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 A60: p +* (i,(m + 1)) in dom (primrec (f1,f2,i)) ; :: thesis:
G . (p +* (i,m)) in rng G by A25, FUNCT_1:def 5;
then dom (G . (p +* (i,m))) in { (dom f) where f is Element of rngG : verum } ;
then p +* (i,m) in union { (dom f) where f is Element of rngG : verum } by A5, A34, A60, TARSKI:def 4;
hence p +* (i,m) in dom (primrec (f1,f2,i)) by A1, Th15; :: thesis:
A61: G . (p +* (i,(m + 1))) in rng G by A25, FUNCT_1:def 5;
dom (G . (p +* (i,m))) c= dom (G . (p +* (i,(m + 1)))) by A4, A2, Lm4;
then (union rngG) . (p +* (i,m)) = (G . (p +* (i,(m + 1)))) . (p +* (i,m)) by A5, A34, A60, A61, Th16;
hence (p +* (i,m)) ^ <*((primrec (f1,f2,i)) . (p +* (i,m)))*> in dom f2 by A1, A5, A34, A60, FUNCT_7:36; :: thesis:

end;

assume that
A62: p +* (i,m) in dom (primrec (f1,f2,i)) and
A63: (p +* (i,m)) ^ <*((primrec (f1,f2,i)) . (p +* (i,m)))*> in dom f2 ; :: thesis:
A64: G . (p +* (i,(m + 1))) in rng G by A25, FUNCT_1:def 5;
G . (p +* (i,(m + 1))) in rng G by A25, FUNCT_1:def 5;
then A65: dom (G . (p +* (i,(m + 1)))) in { (dom f) where f is Element of rngG : verum } ;
A66: dom (G . (p +* (i,m))) c= dom (G . (p +* (i,(m + 1)))) by A4, A2, Lm4;
p +* (i,m) in dom (G . (p +* (i,m))) by A5, A62;
then p +* (i,(m + 1)) in union { (dom f) where f is Element of rngG : verum } by A1, A32, A34, A63, A65, A64, A66, Th16, TARSKI:def 4;
hence p +* (i,(m + 1)) in dom (primrec (f1,f2,i)) by A1, Th15; :: thesis:

end;

assume A67: p +* (i,(m + 1)) in dom (primrec (f1,f2,i)) ; :: thesis:
A68: dom (G . (p +* (i,m))) c= dom (G . (p +* (i,(m + 1)))) by A4, A2, Lm4;
then A69: (union rngG) . (p +* (i,(m + 1))) = (G . (p +* (i,(m + 1)))) . (p +* (i,(m + 1))) by A5, A67, A26, Th16;
(union rngG) . (p +* (i,m)) = (G . (p +* (i,(m + 1)))) . (p +* (i,m)) by A5, A34, A67, A26, A68, Th16;
hence (primrec (f1,f2,i)) . (p +* (i,(m + 1))) = f2 . ((p +* (i,m)) ^ <*((primrec (f1,f2,i)) . (p +* (i,m)))*>) by A1, A5, A34, A67, A69, FUNCT_7:36; :: thesis: