let k be Element of NAT ; :: thesis: for X being set
for A being Subset of X
for A1 being SetSequence of X holds (A1 (\) A) ^\ k = (A1 ^\ k) (\) A
let X be set ; :: thesis: for A being Subset of X
for A1 being SetSequence of X holds (A1 (\) A) ^\ k = (A1 ^\ k) (\) A
let A be Subset of X; :: thesis: for A1 being SetSequence of X holds (A1 (\) A) ^\ k = (A1 ^\ k) (\) A
let A1 be SetSequence of X; :: thesis: (A1 (\) A) ^\ k = (A1 ^\ k) (\) A

now

let n be Element of NAT ; :: thesis: ((A1 (\) A) ^\ k) . n = ((A1 ^\ k) (\) A) . n
thus ((A1 (\) A) ^\ k) . n = (A1 (\) A) . (n + k) by NAT_1:def 3
.= (A1 . (n + k)) \ A by Def8
.= ((A1 ^\ k) . n) \ A by NAT_1:def 3
.= ((A1 ^\ k) (\) A) . n by Def8 ; :: thesis: verum

end;

hence (A1 (\) A) ^\ k = (A1 ^\ k) (\) A by FUNCT_2:113; :: thesis: verum