let k be Nat; :: thesis: for seq, seq1 being Real_Sequence holds (seq + seq1) ^\ k = (seq ^\ k) + (seq1 ^\ k)
let seq, seq1 be Real_Sequence; :: thesis: (seq + seq1) ^\ k = (seq ^\ k) + (seq1 ^\ k)

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

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

end;

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