let k, n be Nat; ((Rascal (k + n)) . (n + 1)) * ((Rascal ((k + n) + 2)) . (n + 2)) = (((Rascal ((k + n) + 1)) . (n + 1)) * ((Rascal ((k + n) + 1)) . (n + 2))) + 1
A0:
( dom (Rascal (k + n)) = Seg ((k + n) + 1) & dom (Rascal ((k + n) + 1)) = Seg (((k + n) + 1) + 1) & dom (Rascal ((k + n) + 2)) = Seg (((k + n) + 2) + 1) )
by Def1;
( 1 + 0 <= 1 + n & 0 + (n + 1) <= k + (n + 1) )
by XREAL_1:6;
then
n + 1 in dom (Rascal (k + n))
by A0;
then A1:
(Rascal (k + n)) . (n + 1) = (((n + 1) - 1) * (((k + n) + 1) - (n + 1))) + 1
by Def1;
( 1 + 0 <= 1 + n & 0 + (n + 1) <= (k + 1) + (n + 1) )
by XREAL_1:6;
then
n + 1 in dom (Rascal ((k + n) + 1))
by A0;
then A2:
(Rascal ((k + n) + 1)) . (n + 1) = (((n + 1) - 1) * ((((k + n) + 1) + 1) - (n + 1))) + 1
by Def1;
( 1 + 0 <= 1 + (n + 1) & 0 + (n + 2) <= k + (n + 2) )
by XREAL_1:6;
then
n + 2 in dom (Rascal ((k + n) + 1))
by A0;
then A3:
(Rascal ((k + n) + 1)) . (n + 2) = (((n + 2) - 1) * ((((k + n) + 1) + 1) - (n + 2))) + 1
by Def1;
( 1 + 0 <= 1 + (n + 1) & 0 + (n + 2) <= (k + 1) + (n + 2) )
by XREAL_1:6;
then
n + 2 in dom (Rascal ((k + n) + 2))
by A0;
then
(Rascal ((k + n) + 2)) . (n + 2) = (((n + 2) - 1) * ((((k + n) + 2) + 1) - (n + 2))) + 1
by Def1;
hence
((Rascal (k + n)) . (n + 1)) * ((Rascal ((k + n) + 2)) . (n + 2)) = (((Rascal ((k + n) + 1)) . (n + 1)) * ((Rascal ((k + n) + 1)) . (n + 2))) + 1
by A1, A2, A3; verum