let i, m be Element of NAT ; :: thesis:
let f1, f2 be non empty to-naturals homogeneous from-natural-fseqs Function; :: thesis:
let p be Element of ((arity f1) + 1) -tuples_on NAT ; :: thesis:
assume A1: i in dom p ; :: thesis:
consider G being Function of ((arity f1) + 1) -tuples_on NAT , HFuncs NAT such that
A2: primrec f1,f2,i = Union G and
A3: for p being Element of ((arity f1) + 1) -tuples_on NAT holds G . p = primrec f1,f2,i,p by Def14;
A4: Union G = union (rng G) by CARD_3:def 4;
then reconsider rngG = rng G as functional compatible set by A2, Th14;
A5: dom G = ((arity f1) + 1) -tuples_on NAT by FUNCT_2:def 1;

A6: now

let k be Element of NAT ; :: thesis:
assume that
A7: p +* i,k in dom (primrec f1,f2,i) and
A8: not p +* i,k in dom (G . (p +* i,k)) ; :: thesis:
set pk = p +* i,k;
union rngG <> {} by A2, A7, CARD_3:def 4, RELAT_1:60;
then reconsider rngG = rng G as non empty functional compatible set ;
dom (union rngG) = union { (dom f) where f is Element of rngG : verum } by Th15;
then consider X being set such that
A9: ( p +* i,k in X & X in { (dom f) where f is Element of rngG : verum } ) by A2, A4, A7, TARSKI:def 4;
consider f being Element of rngG such that
A10: X = dom f by A9;
consider pp being set such that
A11: ( pp in dom G & 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 A3;
then consider m being Element of NAT such that
A12: p +* i,k = pp +* i,m by A9, A10, A11, Th53;
set ppi = pp . i;
A13: p +* i,(pp . i) = (p +* i,k) +* i,(pp . i) by FUNCT_7:36
.= pp +* i,(pp . i) by A12, FUNCT_7:36
.= pp by FUNCT_7:37 ;

per cases by XXREAL_0:1;

suppose k = pp . i ; :: thesis:

hence contradiction by A8, A9, A10, 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 13;
k = (pp . i) + m by A14;
then dom (G . pp) c= dom (G . (p +* i,k)) by A1, A3, A13, Lm4;
hence contradiction by A8, A9, A10, 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 13;
pp . i = k + m by A15;
hence contradiction by A1, A3, A8, A9, A10, A11, A13, Lm5; :: thesis:

end;

set p0 = p +* i,0 ;
A16: dom p = dom (p +* i,0 ) by FUNCT_7:32;

A17: now

A18: G . (p +* i,0 ) = primrec f1,f2,i,(p +* i,0 ) by A3;
consider F being Function of NAT , HFuncs NAT such that
A19: primrec f1,f2,i,(p +* i,0 ) = F . ((p +* i,0 ) /. i) and
A20: ( 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
A21: ( ( 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;
A22: (p +* i,0 ) /. i = (p +* i,0 ) . i by A1, A16, PARTFUN1:def 8
.= 0 by A1, FUNCT_7:33 ;
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 A3, A19, A21, A22, Th6, RELAT_1:60; :: thesis:
assume Del p,i in dom f1 ; :: thesis:
then dom (F . 0 ) = {((p +* i,0 ) +* i,0 )} by A1, A20, 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 A18, A19, A22, 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 A3, A19, A20, A21, A22, FUNCT_7:36, RELAT_1:60;
then ( F . 0 = {(p +* i,0 )} --> (f1 . (Del p,i)) & p +* i,0 in {(p +* i,0 )} ) by Th6, TARSKI:def 1;
hence (G . (p +* i,0 )) . (p +* i,0 ) = f1 . (Del p,i) by A18, A19, A22, FUNCOP_1:13; :: thesis:

end;

A23: G . (p +* i,0 ) in rng G by A5, FUNCT_1:def 5;
reconsider rngG = rngG as non empty functional compatible set ;
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 A6, A17; :: thesis:
assume A24: Del p,i in dom f1 ; :: thesis:
dom (G . (p +* i,0 )) in { (dom f) where f is Element of rngG : verum } by A23;
then p +* i,0 in union { (dom f) where f is Element of rngG : verum } by A17, A24, TARSKI:def 4;
hence p +* i,0 in dom (primrec f1,f2,i) by A2, A4, Th15; :: thesis:

end;

hereby :: thesis:

assume A25: p +* i,0 in dom (primrec f1,f2,i) ; :: thesis:
then p +* i,0 in dom (G . (p +* i,0 )) by A6;
then (union rngG) . (p +* i,0 ) = (G . (p +* i,0 )) . (p +* i,0 ) by A23, Th16;
hence (primrec f1,f2,i) . (p +* i,0 ) = f1 . (Del p,i) by A2, A6, A17, A25, CARD_3:def 4; :: 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))*>;
A26: ( dom p = dom (p +* i,(m + 1)) & dom p = dom (p +* i,m) ) by FUNCT_7:32;
A27: ( (p +* i,(m + 1)) +* i,m = p +* i,m & (p +* i,(m + 1)) +* i,(m + 1) = p +* i,(m + 1) ) by FUNCT_7:36;

A28: now

A29: ( G . (p +* i,(m + 1)) = primrec f1,f2,i,(p +* i,(m + 1)) & G . (p +* i,m) = primrec f1,f2,i,(p +* i,m) ) by A3;
consider F1 being Function of NAT , HFuncs NAT such that
A30: primrec f1,f2,i,(p +* i,(m + 1)) = F1 . ((p +* i,(m + 1)) /. i) and
A31: ( ( 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)) ) & ( ( not i in dom (p +* i,(m + 1)) or not Del (p +* i,(m + 1)),i in dom f1 ) implies F1 . 0 = {} ) ) and
A32: for M being Element of NAT holds S₁[M,F1 . M,F1 . (M + 1),p +* i,(m + 1),i,f2] by Def13;
consider F being Function of NAT , HFuncs NAT such that
A33: primrec f1,f2,i,(p +* i,m) = F . ((p +* i,m) /. i) and
A34: ( ( 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)) ) & ( ( not i in dom (p +* i,m) or not Del (p +* i,m),i in dom f1 ) implies F . 0 = {} ) ) and
A35: for M being Element of NAT holds S₁[M,F . M,F . (M + 1),p +* i,m,i,f2] by Def13;
A36: (p +* i,(m + 1)) /. i = (p +* i,(m + 1)) . i by A1, A26, PARTFUN1:def 8
.= m + 1 by A1, FUNCT_7:33 ;
A37: (p +* i,m) /. i = (p +* i,m) . i by A1, A26, PARTFUN1:def 8
.= m by A1, FUNCT_7:33 ;
A38: F1 . m = F . m by A31, A32, A34, A35, Lm2;
A39: (F1 . (m + 1)) . (p +* i,m) = (F1 . m) . (p +* i,m) by A1, A31, A32, Lm3;
A40: not p +* i,(m + 1) in dom (F1 . m) by A1, A31, A32, Lm3;
thus A41: ( 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 A42: p +* i,(m + 1) in dom (G . (p +* i,(m + 1))) ; :: thesis:
then A43: p +* i,(m + 1) in dom (F1 . (m + 1)) by A3, A30, A36;
assume A44: ( 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 A44;

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

then not p +* i,m in dom (F1 . m) by A3, A33, A37, A38;
hence contradiction by A27, A32, A40, A43; :: 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 A27, A29, A30, A32, A36, A39, A40, A42; :: thesis:

end;

assume ( 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:
then A45: F1 . (m + 1) = (F1 . m) +* ((p +* i,(m + 1)) .--> (f2 . ((p +* i,m) ^ <*((F1 . m) . (p +* i,m))*>))) by A1, A26, A27, A29, A30, A32, A33, A36, A37, A38, A39;
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 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;
hence p +* i,(m + 1) in dom (G . (p +* i,(m + 1))) by A29, A30, A36, A45, FUNCT_4:def 1; :: thesis:

end;

assume A46: 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 A27, A29, A30, A32, A36, A41;
then A47: F1 . (m + 1) = (F1 . m) +* ((p +* i,(m + 1)) .--> (f2 . ((p +* i,m) ^ <*((F1 . m) . (p +* i,m))*>))) by A1, A26, A27, A29, A32, A33, A37, A38, A41, A46;
A48: 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;
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 A29, A30, A36, A47, FUNCT_4:14
.= f2 . ((p +* i,m) ^ <*((G . (p +* i,(m + 1))) . ((p +* i,(m + 1)) +* i,m))*>) by A27, A29, A30, A36, A39, A48, 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 A49: p +* i,(m + 1) in dom (primrec f1,f2,i) ; :: thesis:
G . (p +* i,m) in rng G by A5, 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 A6, A28, A49, TARSKI:def 4;
hence p +* i,m in dom (primrec f1,f2,i) by A2, A4, Th15; :: thesis:
A50: G . (p +* i,(m + 1)) in rng G by A5, FUNCT_1:def 5;
dom (G . (p +* i,m)) c= dom (G . (p +* i,(m + 1))) by A1, A3, Lm4;
then (union rngG) . (p +* i,m) = (G . (p +* i,(m + 1))) . (p +* i,m) by A6, A28, A49, A50, Th16;
hence (p +* i,m) ^ <*((primrec f1,f2,i) . (p +* i,m))*> in dom f2 by A2, A6, A27, A28, A49, CARD_3:def 4; :: thesis:

end;

assume A51: ( p +* i,m in dom (primrec f1,f2,i) & (p +* i,m) ^ <*((primrec f1,f2,i) . (p +* i,m))*> in dom f2 ) ; :: thesis:
then A52: p +* i,m in dom (G . (p +* i,m)) by A6;
A53: G . (p +* i,(m + 1)) in rng G by A5, FUNCT_1:def 5;
dom (G . (p +* i,m)) c= dom (G . (p +* i,(m + 1))) by A1, A3, Lm4;
then A54: (union rngG) . (p +* i,m) = (G . (p +* i,(m + 1))) . (p +* i,m) by A52, A53, Th16;
G . (p +* i,(m + 1)) in rng G by A5, FUNCT_1:def 5;
then dom (G . (p +* i,(m + 1))) in { (dom f) where f is Element of rngG : verum } ;
then p +* i,(m + 1) in union { (dom f) where f is Element of rngG : verum } by A2, A6, A27, A28, A51, A54, CARD_3:def 4, TARSKI:def 4;
hence p +* i,(m + 1) in dom (primrec f1,f2,i) by A2, A4, Th15; :: thesis:

end;

assume A55: p +* i,(m + 1) in dom (primrec f1,f2,i) ; :: thesis:
A56: G . (p +* i,(m + 1)) in rng G by A5, FUNCT_1:def 5;
dom (G . (p +* i,m)) c= dom (G . (p +* i,(m + 1))) by A1, A3, Lm4;
then ( (union rngG) . (p +* i,m) = (G . (p +* i,(m + 1))) . (p +* i,m) & (union rngG) . (p +* i,(m + 1)) = (G . (p +* i,(m + 1))) . (p +* i,(m + 1)) ) by A6, A28, A55, A56, Th16;
hence (primrec f1,f2,i) . (p +* i,(m + 1)) = f2 . ((p +* i,m) ^ <*((primrec f1,f2,i) . (p +* i,m))*>) by A2, A4, A6, A28, A55, FUNCT_7:36; :: thesis: