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

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