let k be Element of 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)
thus (seq /" seq1) ^\ k = (seq ^\ k) (#) ((seq1 ") ^\ k) by Th42
.= (seq ^\ k) /" (seq1 ^\ k) by Th41 ; :: thesis: verum