let n be Nat; :: thesis: for f, g being Element of Permutations n holds f * g in Permutations n
let f, g be Element of Permutations n; :: thesis: f * g in Permutations n
reconsider F = f, G = g as Permutation of (Seg n) by MATRIX_1:def 12;
F * G is Permutation of (Seg n) ;
hence f * g in Permutations n by MATRIX_1:def 12; :: thesis: verum