let X be ComplexUnitarySpace; :: thesis: for seq1, seq2 being sequence of X
for k being Nat holds (seq1 + seq2) ^\ k = (seq1 ^\ k) + (seq2 ^\ k)
let seq1, seq2 be sequence of X; :: thesis: for k being Nat holds (seq1 + seq2) ^\ k = (seq1 ^\ k) + (seq2 ^\ k)
let k be Nat; :: thesis: (seq1 + seq2) ^\ k = (seq1 ^\ k) + (seq2 ^\ k)

now :: thesis: for n being Element of NAT holds ((seq1 + seq2) ^\ k) . n = ((seq1 ^\ k) + (seq2 ^\ k)) . n

let n be Element of NAT ; :: thesis: ((seq1 + seq2) ^\ k) . n = ((seq1 ^\ k) + (seq2 ^\ k)) . n
thus ((seq1 + seq2) ^\ k) . n = (seq1 + seq2) . (n + k) by NAT_1:def 3
.= (seq1 . (n + k)) + (seq2 . (n + k)) by NORMSP_1:def 2
.= ((seq1 ^\ k) . n) + (seq2 . (n + k)) by NAT_1:def 3
.= ((seq1 ^\ k) . n) + ((seq2 ^\ k) . n) by NAT_1:def 3
.= ((seq1 ^\ k) + (seq2 ^\ k)) . n by NORMSP_1:def 2 ; :: thesis: verum

end;

hence (seq1 + seq2) ^\ k = (seq1 ^\ k) + (seq2 ^\ k) by FUNCT_2:63; :: thesis: verum