let i be Element of NAT ; :: thesis: for f1, f2 being non empty NAT * -defined to-naturals homogeneous Function st f1 is len-total & f2 is len-total & (arity f1) + 2 = arity f2 & 1 <= i & i <= 1 + (arity f1) holds
( dom (primrec f1,f2,i) = ((arity f1) + 1) -tuples_on NAT & arity (primrec f1,f2,i) = (arity f1) + 1 )
let f1, f2 be non empty NAT * -defined to-naturals homogeneous Function; :: thesis: ( f1 is len-total & f2 is len-total & (arity f1) + 2 = arity f2 & 1 <= i & i <= 1 + (arity f1) implies ( dom (primrec f1,f2,i) = ((arity f1) + 1) -tuples_on NAT & arity (primrec f1,f2,i) = (arity f1) + 1 ) )
assume that
A1:
f1 is len-total
and
A2:
f2 is len-total
and
A3:
(arity f1) + 2 = arity f2
and
A4:
( 1 <= i & i <= 1 + (arity f1) )
; :: thesis: ( dom (primrec f1,f2,i) = ((arity f1) + 1) -tuples_on NAT & arity (primrec f1,f2,i) = (arity f1) + 1 )
A5:
dom (primrec f1,f2,i) c= ((arity f1) + 1) -tuples_on NAT
by Th60;
set n = (arity f1) + 1;
((arity f1) + 1) -tuples_on NAT c= dom (primrec f1,f2,i)
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in ((arity f1) + 1) -tuples_on NAT or x in dom (primrec f1,f2,i) )
assume A6:
x in ((arity f1) + 1) -tuples_on NAT
;
:: thesis: x in dom (primrec f1,f2,i)
reconsider x' =
x as
Element of
((arity f1) + 1) -tuples_on NAT by A6;
consider G being
Function of
(((arity f1) + 1) -tuples_on NAT ),
(HFuncs NAT ) such that A7:
primrec f1,
f2,
i = Union G
and A8:
for
p being
Element of
((arity f1) + 1) -tuples_on NAT holds
G . p = primrec f1,
f2,
i,
p
by Def14;
A9:
G . x' = primrec f1,
f2,
i,
x'
by A8;
A10:
x' in dom (primrec f1,f2,i,x')
by A1, A2, A3, A4, Th58;
dom G = ((arity f1) + 1) -tuples_on NAT
by FUNCT_2:def 1;
then A11:
G . x' in rng G
by FUNCT_1:12;
Union G = union (rng G)
by CARD_3:def 4;
then reconsider rngG =
rng G as non
empty functional compatible set by A7, Th14;
A12:
dom (union rngG) = union { (dom f) where f is Element of rngG : verum }
by Th15;
dom (G . x') in { (dom f) where f is Element of rngG : verum }
by A11;
then
x in dom (union rngG)
by A9, A10, A12, TARSKI:def 4;
hence
x in dom (primrec f1,f2,i)
by A7, CARD_3:def 4;
:: thesis: verum
end;
hence
dom (primrec f1,f2,i) = ((arity f1) + 1) -tuples_on NAT
by A5, XBOOLE_0:def 10; :: thesis: arity (primrec f1,f2,i) = (arity f1) + 1
hence
arity (primrec f1,f2,i) = (arity f1) + 1
by Th28; :: thesis: verum