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