let k, n be Nat; :: thesis: for f being natural-valued Function st n > 1 holds
Coim ((n |^ f),(n |^ k)) = Coim (f,k)
let f be natural-valued Function; :: thesis: ( n > 1 implies Coim ((n |^ f),(n |^ k)) = Coim (f,k) )
assume A1: n > 1 ; :: thesis: Coim ((n |^ f),(n |^ k)) = Coim (f,k)
thus Coim ((n |^ f),(n |^ k)) c= Coim (f,k) :: according to XBOOLE_0:def 10 :: thesis: Coim (f,k) c= Coim ((n |^ f),(n |^ k))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Coim ((n |^ f),(n |^ k)) or x in Coim (f,k) )
assume x in Coim ((n |^ f),(n |^ k)) ; :: thesis: x in Coim (f,k)
then x in (n |^ f) " {(n |^ k)} by RELAT_1:def 17;
then ( x in dom (n |^ f) & (n |^ f) . x in {(n |^ k)} ) by FUNCT_1:def 7;
then A2: ( x in dom f & (n |^ f) . x = n |^ k ) by TARSKI:def 1, Def4;
then (n |^ f) . x = n to_power (f . x) by Def4
.= n |^ (f . x) ;
then k = f . x by A2, A1, PEPIN:30;
then f . x in {k} by TARSKI:def 1;
then x in f " {k} by A2, FUNCT_1:def 7;
hence x in Coim (f,k) by RELAT_1:def 17; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Coim (f,k) or x in Coim ((n |^ f),(n |^ k)) )
assume x in Coim (f,k) ; :: thesis: x in Coim ((n |^ f),(n |^ k))
then x in f " {k} by RELAT_1:def 17;
then A3: ( x in dom f & f . x in {k} ) by FUNCT_1:def 7;
then A4: ( f . x = k & x in dom (n |^ f) ) by TARSKI:def 1, Def4;
then (n |^ f) . x = n to_power k by Def4, A3
.= n |^ k ;
then (n |^ f) . x in {(n |^ k)} by TARSKI:def 1;
then x in (n |^ f) " {(n |^ k)} by FUNCT_1:def 7, A4;
hence x in Coim ((n |^ f),(n |^ k)) by RELAT_1:def 17; :: thesis: verum