begin
definition
let n1,
n2 be
Element of
NAT ;
existence
ex b1 being sequence of NAT st
for n being Element of NAT holds b1 . n = IFGT (n,n1,(n + n2),n)
uniqueness
for b1, b2 being sequence of NAT st ( for n being Element of NAT holds b1 . n = IFGT (n,n1,(n + n2),n) ) & ( for n being Element of NAT holds b2 . n = IFGT (n,n1,(n + n2),n) ) holds
b1 = b2
end;
definition
let k be
Element of
NAT ;
existence
ex b1 being sequence of NAT st
for n being Element of NAT holds b1 . n = IFGT (n,k,0,1)
uniqueness
for b1, b2 being sequence of NAT st ( for n being Element of NAT holds b1 . n = IFGT (n,k,0,1) ) & ( for n being Element of NAT holds b2 . n = IFGT (n,k,0,1) ) holds
b1 = b2
end;
definition
let n1,
n2 be
Element of
NAT ;
existence
ex b1 being sequence of NAT st
for n being Element of NAT holds b1 . n = IFGT (n,(n1 + 1),(n + n2),n)
uniqueness
for b1, b2 being sequence of NAT st ( for n being Element of NAT holds b1 . n = IFGT (n,(n1 + 1),(n + n2),n) ) & ( for n being Element of NAT holds b2 . n = IFGT (n,(n1 + 1),(n + n2),n) ) holds
b1 = b2
end;