let n be Element of NAT ; :: thesis: ( n > 0 implies ex Catal being XFinSequence of st
( Sum Catal = Catalan (n + 1) & dom Catal = n & ( for j being Element of NAT st j < n holds
Catal . j = (Catalan (j + 1)) * (Catalan (n -' j)) ) ) )
assume A1: n > 0 ; :: thesis: ex Catal being XFinSequence of st
( Sum Catal = Catalan (n + 1) & dom Catal = n & ( for j being Element of NAT st j < n holds
Catal . j = (Catalan (j + 1)) * (Catalan (n -' j)) ) )
consider CardF being XFinSequence of such that
A2: card { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (2 * n),n & { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } <> {} ) } = Sum CardF and
A3: dom CardF = n and
A4: for j being Element of 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 Th41;
take CardF ; :: thesis: ( Sum CardF = Catalan (n + 1) & dom CardF = n & ( for j being Element of NAT st j < n holds
CardF . j = (Catalan (j + 1)) * (Catalan (n -' j)) ) )
Sum CardF = card (Domin_0 (2 * n),n) by A1, A2, Th42;
hence ( Sum CardF = Catalan (n + 1) & dom CardF = n ) by A3, Th38; :: thesis: for j being Element of NAT st j < n holds
CardF . j = (Catalan (j + 1)) * (Catalan (n -' j))
let j be Element of 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 = n - j & n - j > j - j ) by A5, XREAL_1:11, XREAL_1:235;
then n -' j > 0 ;
then reconsider nj = (n -' j) - 1 as Element of NAT by NAT_1:20;
j + 1 <= n by A5, NAT_1:13;
then ( (2 * n) -' (2 * (j + 1)) = (2 * n) - (2 * (j + 1)) & n -' (j + 1) = n - (j + 1) & n - j = n -' j ) by A5, XREAL_1:66, XREAL_1:235;
then A6: card (Domin_0 ((2 * n) -' (2 * (j + 1))),(n -' (j + 1))) = card (Domin_0 (2 * nj),nj)
.= Catalan (nj + 1) by Th38 ;
card (Domin_0 (2 * j),j) = Catalan (j + 1) by Th38;
hence CardF . j = (Catalan (j + 1)) * (Catalan (n -' j)) by A4, A5, A6; :: thesis: verum