let a, b be Complex; :: thesis: for n, k being Nat st k in Segm (n + 1) holds
ex c being object ex l being Nat st
( l = n - k & c = (a |^ l) * (b |^ k) )
let n, k be Nat; :: thesis: ( k in Segm (n + 1) implies ex c being object ex l being Nat st
( l = n - k & c = (a |^ l) * (b |^ k) ) )
assume k in Segm (n + 1) ; :: thesis: ex c being object ex l being Nat st
( l = n - k & c = (a |^ l) * (b |^ k) )
then reconsider l1 = n - k as Nat by LmA;
(a |^ l1) * (b |^ k) is object ;
hence ex c being object ex l being Nat st
( l = n - k & c = (a |^ l) * (b |^ k) ) ; :: thesis: verum