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