per cases ( k in dom ((0,0) In_Power n) or not k in dom ((0,0) In_Power n) ) ;
suppose A1: k in dom ((0,0) In_Power n) ; :: thesis: ((0,0) In_Power n) . k is zero
then A2: ( 1 <= k & k <= len ((0,0) In_Power ((n + 1) - 1)) ) by FINSEQ_3:25;
then reconsider m = k - 1 as Nat ;
ex l being Nat st n + 1 = (m + 1) + l by A2, NAT_1:10;
then reconsider l = n - m as Nat ;
( m = 0 implies l >= 1 ) by NAT_1:14;
then A3: ( m < 1 implies 0 |^ l = 0 ) by NAT_1:14, NEWTON:11;
A4: ( m >= 1 implies 0 |^ m = 0 ) by NEWTON:11;
((0,0) In_Power ((n + 1) - 1)) . k = ((n choose m) * (0 |^ l)) * (0 |^ m) by A1, NEWTON:def 4;
hence ((0,0) In_Power n) . k is zero by A3, A4; :: thesis: verum
end;
suppose not k in dom ((0,0) In_Power n) ; :: thesis: ((0,0) In_Power n) . k is zero
hence ((0,0) In_Power n) . k is zero by FUNCT_1:def 2; :: thesis: verum
end;
end;