let n be Nat; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ( 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; :: thesis: for j being Nat st j < n holds
CardF . j = (Catalan (j + 1)) * (Catalan (n -' j))
let j be Nat; :: thesis: ( j < n implies CardF . j = (Catalan (j + 1)) * (Catalan (n -' j)) )
assume A5: j < n ; :: thesis: 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; :: thesis: verum