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 h is total 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 h is total holds
h /* (s ^\ n) = (h /* s) ^\ n
let h be PartFunc of X,Y; :: thesis: for n being Nat st h is total holds
h /* (s ^\ n) = (h /* s) ^\ n
let n be Nat; :: thesis: ( h is total implies h /* (s ^\ n) = (h /* s) ^\ n )
assume h is total ; :: thesis: h /* (s ^\ n) = (h /* s) ^\ n
then dom h = X by PARTFUN1:def 2;
then rng s c= dom h ;
hence h /* (s ^\ n) = (h /* s) ^\ n by Th27; :: thesis: verum