let k be Nat; :: thesis: for X being set
for A being Subset of X
for A1 being SetSequence of X holds (A (\+\) A1) ^\ k = A (\+\) (A1 ^\ k)
let X be set ; :: thesis: for A being Subset of X
for A1 being SetSequence of X holds (A (\+\) A1) ^\ k = A (\+\) (A1 ^\ k)
let A be Subset of X; :: thesis: for A1 being SetSequence of X holds (A (\+\) A1) ^\ k = A (\+\) (A1 ^\ k)
let A1 be SetSequence of X; :: thesis: (A (\+\) A1) ^\ k = A (\+\) (A1 ^\ k)
let n be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: ((A (\+\) A1) ^\ k) . n = (A (\+\) (A1 ^\ k)) . n
thus ((A (\+\) A1) ^\ k) . n = (A (\+\) A1) . (n + k) by NAT_1:def 3
.= A \+\ (A1 . (n + k)) by Def9
.= A \+\ ((A1 ^\ k) . n) by NAT_1:def 3
.= (A (\+\) (A1 ^\ k)) . n by Def9 ; :: thesis: verum