let i, m be Element of NAT ; :: thesis: for f1, f2 being non empty NAT * -defined to-naturals homogeneous Function
for p being Element of ((arity f1) + 1) -tuples_on NAT st i in dom p holds
( ( p +* i,0 in dom (primrec f1,f2,i) implies Del p,i in dom f1 ) & ( Del p,i in dom f1 implies p +* i,0 in dom (primrec f1,f2,i) ) & ( p +* i,0 in dom (primrec f1,f2,i) implies (primrec f1,f2,i) . (p +* i,0 ) = f1 . (Del p,i) ) & ( p +* i,(m + 1) in dom (primrec f1,f2,i) implies ( p +* i,m in dom (primrec f1,f2,i) & (p +* i,m) ^ <*((primrec f1,f2,i) . (p +* i,m))*> in dom f2 ) ) & ( p +* i,m in dom (primrec f1,f2,i) & (p +* i,m) ^ <*((primrec f1,f2,i) . (p +* i,m))*> in dom f2 implies p +* i,(m + 1) in dom (primrec f1,f2,i) ) & ( p +* i,(m + 1) in dom (primrec f1,f2,i) implies (primrec f1,f2,i) . (p +* i,(m + 1)) = f2 . ((p +* i,m) ^ <*((primrec f1,f2,i) . (p +* i,m))*>) ) )
let f1, f2 be non empty NAT * -defined to-naturals homogeneous Function; :: thesis: for p being Element of ((arity f1) + 1) -tuples_on NAT st i in dom p holds
( ( p +* i,0 in dom (primrec f1,f2,i) implies Del p,i in dom f1 ) & ( Del p,i in dom f1 implies p +* i,0 in dom (primrec f1,f2,i) ) & ( p +* i,0 in dom (primrec f1,f2,i) implies (primrec f1,f2,i) . (p +* i,0 ) = f1 . (Del p,i) ) & ( p +* i,(m + 1) in dom (primrec f1,f2,i) implies ( p +* i,m in dom (primrec f1,f2,i) & (p +* i,m) ^ <*((primrec f1,f2,i) . (p +* i,m))*> in dom f2 ) ) & ( p +* i,m in dom (primrec f1,f2,i) & (p +* i,m) ^ <*((primrec f1,f2,i) . (p +* i,m))*> in dom f2 implies p +* i,(m + 1) in dom (primrec f1,f2,i) ) & ( p +* i,(m + 1) in dom (primrec f1,f2,i) implies (primrec f1,f2,i) . (p +* i,(m + 1)) = f2 . ((p +* i,m) ^ <*((primrec f1,f2,i) . (p +* i,m))*>) ) )
let p be Element of ((arity f1) + 1) -tuples_on NAT ; :: thesis: ( i in dom p implies ( ( p +* i,0 in dom (primrec f1,f2,i) implies Del p,i in dom f1 ) & ( Del p,i in dom f1 implies p +* i,0 in dom (primrec f1,f2,i) ) & ( p +* i,0 in dom (primrec f1,f2,i) implies (primrec f1,f2,i) . (p +* i,0 ) = f1 . (Del p,i) ) & ( p +* i,(m + 1) in dom (primrec f1,f2,i) implies ( p +* i,m in dom (primrec f1,f2,i) & (p +* i,m) ^ <*((primrec f1,f2,i) . (p +* i,m))*> in dom f2 ) ) & ( p +* i,m in dom (primrec f1,f2,i) & (p +* i,m) ^ <*((primrec f1,f2,i) . (p +* i,m))*> in dom f2 implies p +* i,(m + 1) in dom (primrec f1,f2,i) ) & ( p +* i,(m + 1) in dom (primrec f1,f2,i) implies (primrec f1,f2,i) . (p +* i,(m + 1)) = f2 . ((p +* i,m) ^ <*((primrec f1,f2,i) . (p +* i,m))*>) ) ) )
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: ( ( p +* i,0 in dom (primrec f1,f2,i) implies Del p,i in dom f1 ) & ( Del p,i in dom f1 implies p +* i,0 in dom (primrec f1,f2,i) ) & ( p +* i,0 in dom (primrec f1,f2,i) implies (primrec f1,f2,i) . (p +* i,0 ) = f1 . (Del p,i) ) & ( p +* i,(m + 1) in dom (primrec f1,f2,i) implies ( p +* i,m in dom (primrec f1,f2,i) & (p +* i,m) ^ <*((primrec f1,f2,i) . (p +* i,m))*> in dom f2 ) ) & ( p +* i,m in dom (primrec f1,f2,i) & (p +* i,m) ^ <*((primrec f1,f2,i) . (p +* i,m))*> in dom f2 implies p +* i,(m + 1) in dom (primrec f1,f2,i) ) & ( p +* i,(m + 1) in dom (primrec f1,f2,i) implies (primrec f1,f2,i) . (p +* i,(m + 1)) = f2 . ((p +* i,m) ^ <*((primrec f1,f2,i) . (p +* i,m))*>) ) )

A5: now

let k be Element of NAT ; :: thesis: ( p +* i,k in dom (primrec f1,f2,i) implies p +* i,k in dom (G . (p +* i,k)) )
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: contradiction
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 ( k = pp . i or pp . i < k or pp . i > k ) by XXREAL_0:1;

suppose k = pp . i ; :: thesis: contradiction

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

end;

suppose pp . i < k ; :: thesis: contradiction

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: verum

end;

suppose pp . i > k ; :: thesis: contradiction

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: verum

end;

end;

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: ( p +* i,0 in dom (G . (p +* i,0 )) implies (G . (p +* i,0 )) . (p +* i,0 ) = f1 . (Del p,i) )

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: ( Del p,i in dom f1 implies p +* i,0 in dom (G . (p +* i,0 )) )
assume Del p,i in dom f1 ; :: thesis: p +* i,0 in dom (G . (p +* i,0 ))
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: verum

end;

assume p +* i,0 in dom (G . (p +* i,0 )) ; :: thesis: (G . (p +* i,0 )) . (p +* i,0 ) = f1 . (Del p,i)
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: verum

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: ( ( p +* i,0 in dom (primrec f1,f2,i) implies (primrec f1,f2,i) . (p +* i,0 ) = f1 . (Del p,i) ) & ( p +* i,(m + 1) in dom (primrec f1,f2,i) implies ( p +* i,m in dom (primrec f1,f2,i) & (p +* i,m) ^ <*((primrec f1,f2,i) . (p +* i,m))*> in dom f2 ) ) & ( p +* i,m in dom (primrec f1,f2,i) & (p +* i,m) ^ <*((primrec f1,f2,i) . (p +* i,m))*> in dom f2 implies p +* i,(m + 1) in dom (primrec f1,f2,i) ) & ( p +* i,(m + 1) in dom (primrec f1,f2,i) implies (primrec f1,f2,i) . (p +* i,(m + 1)) = f2 . ((p +* i,m) ^ <*((primrec f1,f2,i) . (p +* i,m))*>) ) )

proof

thus ( p +* i,0 in dom (primrec f1,f2,i) implies Del p,i in dom f1 ) by A5, A18; :: thesis: ( Del p,i in dom f1 implies p +* i,0 in dom (primrec f1,f2,i) )
assume A28: Del p,i in dom f1 ; :: thesis: p +* i,0 in dom (primrec f1,f2,i)
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: verum

end;

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

assume A29: p +* i,0 in dom (primrec f1,f2,i) ; :: thesis: (primrec f1,f2,i) . (p +* i,0 ) = f1 . (Del p,i)
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: verum

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: ( p +* i,(m + 1) in dom (G . (p +* i,(m + 1))) implies (G . (p +* i,(m + 1))) . (p +* i,(m + 1)) = f2 . ((p +* i,m) ^ <*((G . (p +* i,(m + 1))) . ((p +* i,(m + 1)) +* i,m))*>) )

proof

hereby :: thesis: ( 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 implies p +* i,(m + 1) in dom (G . (p +* i,(m + 1))) )

assume A53: p +* i,(m + 1) in dom (G . (p +* i,(m + 1))) ; :: thesis: ( 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 )
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: contradiction

per cases ( 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 ) by A55;

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

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

end;

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

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

end;

end;

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 dom (G . (p +* i,(m + 1)))
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: verum

end;

assume A59: p +* i,(m + 1) in dom (G . (p +* i,(m + 1))) ; :: thesis: (G . (p +* i,(m + 1))) . (p +* i,(m + 1)) = f2 . ((p +* i,m) ^ <*((G . (p +* i,(m + 1))) . ((p +* i,(m + 1)) +* i,m))*>)
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: verum

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: ( p +* i,(m + 1) in dom (primrec f1,f2,i) implies (primrec f1,f2,i) . (p +* i,(m + 1)) = f2 . ((p +* i,m) ^ <*((primrec f1,f2,i) . (p +* i,m))*>) )

proof

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

assume A60: p +* i,(m + 1) in dom (primrec f1,f2,i) ; :: thesis: ( p +* i,m in dom (primrec f1,f2,i) & (p +* i,m) ^ <*((primrec f1,f2,i) . (p +* i,m))*> in dom f2 )
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: (p +* i,m) ^ <*((primrec f1,f2,i) . (p +* i,m))*> in dom f2
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: verum

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: p +* i,(m + 1) in dom (primrec f1,f2,i)
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: verum

end;

assume A67: p +* i,(m + 1) in dom (primrec f1,f2,i) ; :: thesis: (primrec f1,f2,i) . (p +* i,(m + 1)) = f2 . ((p +* i,m) ^ <*((primrec f1,f2,i) . (p +* i,m))*>)
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: verum