let a, b be Complex; :: thesis: for n, k being Nat st k in Seg (n + 1) holds
ex c being object ex l, m being Nat st
( m = k - 1 & l = n - m & c = (a |^ l) * (b |^ m) )
let n, k be Nat; :: thesis: ( k in Seg (n + 1) implies ex c being object ex l, m being Nat st
( m = k - 1 & l = n - m & c = (a |^ l) * (b |^ m) ) )
assume B1: k in Seg (n + 1) ; :: thesis: ex c being object ex l, m being Nat st
( m = k - 1 & l = n - m & c = (a |^ l) * (b |^ m) )
consider m1, l1 being Nat such that
B2: ( m1 = k - 1 & l1 = n - m1 ) by B1, LmN;
(a |^ l1) * (b |^ m1) is object ;
hence ex c being object ex l, m being Nat st
( m = k - 1 & l = n - m & c = (a |^ l) * (b |^ m) ) by B2; :: thesis: verum