let n be Nat; ( n > 0 implies ex Catal being XFinSequence of NAT st
( Sum Catal = Catalan (n + 1) & dom Catal = n & ( for j being Nat st j < n holds
Catal . j = (Catalan (j + 1)) * (Catalan (n -' j)) ) ) )
assume A1:
n > 0
; ex Catal being XFinSequence of NAT st
( Sum Catal = Catalan (n + 1) & dom Catal = n & ( for j being Nat st j < n holds
Catal . j = (Catalan (j + 1)) * (Catalan (n -' j)) ) )
consider CardF being XFinSequence of NAT such that
A2:
card { pN where pN is Element of NAT ^omega : ( pN in Domin_0 ((2 * n),n) & { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } <> {} ) } = Sum CardF
and
A3:
dom CardF = n
and
A4:
for j being Nat st j < n holds
CardF . j = (card (Domin_0 ((2 * j),j))) * (card (Domin_0 (((2 * n) -' (2 * (j + 1))),(n -' (j + 1)))))
by Th37;
take
CardF
; ( Sum CardF = Catalan (n + 1) & dom CardF = n & ( for j being Nat st j < n holds
CardF . j = (Catalan (j + 1)) * (Catalan (n -' j)) ) )
Sum CardF = card (Domin_0 ((2 * n),n))
by A1, A2, Th38;
hence
( Sum CardF = Catalan (n + 1) & dom CardF = n )
by A3, Th34; for j being Nat st j < n holds
CardF . j = (Catalan (j + 1)) * (Catalan (n -' j))
let j be Nat; ( j < n implies CardF . j = (Catalan (j + 1)) * (Catalan (n -' j)) )
assume A5:
j < n
; CardF . j = (Catalan (j + 1)) * (Catalan (n -' j))
n - j > j - j
by A5, XREAL_1:9;
then
n -' j > 0
by A5, XREAL_1:233;
then reconsider nj = (n -' j) - 1 as Nat by NAT_1:20;
j + 1 <= n
by A5, NAT_1:13;
then A6:
( (2 * n) -' (2 * (j + 1)) = (2 * n) - (2 * (j + 1)) & n -' (j + 1) = n - (j + 1) )
by XREAL_1:64, XREAL_1:233;
A7:
card (Domin_0 ((2 * j),j)) = Catalan (j + 1)
by Th34;
n - j = n -' j
by A5, XREAL_1:233;
then card (Domin_0 (((2 * n) -' (2 * (j + 1))),(n -' (j + 1)))) =
card (Domin_0 ((2 * nj),nj))
by A6
.=
Catalan (nj + 1)
by Th34
;
hence
CardF . j = (Catalan (j + 1)) * (Catalan (n -' j))
by A4, A5, A7; verum