let X, Y be non empty set ; :: thesis: for s being sequence of X
for h being PartFunc of X,Y
for n being Nat st rng s c= dom h holds
(h /* s) ^\ n = h /* (s ^\ n)
let s be sequence of X; :: thesis: for h being PartFunc of X,Y
for n being Nat st rng s c= dom h holds
(h /* s) ^\ n = h /* (s ^\ n)
let h be PartFunc of X,Y; :: thesis: for n being Nat st rng s c= dom h holds
(h /* s) ^\ n = h /* (s ^\ n)
let n be Nat; :: thesis: ( rng s c= dom h implies (h /* s) ^\ n = h /* (s ^\ n) )
assume A1: rng s c= dom h ; :: thesis: (h /* s) ^\ n = h /* (s ^\ n)
let m be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: ((h /* s) ^\ n) . m = (h /* (s ^\ n)) . m
A2: rng (s ^\ n) c= rng s by Th21;
reconsider mn = m + n as Element of NAT by ORDINAL1:def 12;
thus ((h /* s) ^\ n) . m = (h /* s) . (m + n) by NAT_1:def 3
.= h . (s . mn) by A1, FUNCT_2:108
.= h . ((s ^\ n) . m) by NAT_1:def 3
.= (h /* (s ^\ n)) . m by A1, A2, FUNCT_2:108, XBOOLE_1:1 ; :: thesis: verum