let B be permutation of A; :: thesis: B is X -valued
ex f being Permutation of (dom A) st B = A * f by Def9;
hence B is X -valued ; :: thesis: verum