set G = SymGroup {};
A1: the carrier of (SymGroup {}) = permutations {} by Def2;

now

let x, y be Element of 1; :: thesis: the multF of (SymGroup {}) . (x,y) = op2 . (x,y)
reconsider f = x, g = y as Element of (SymGroup {}) by Th4, Def2;
thus the multF of (SymGroup {}) . (x,y) = f * g
.= {} by A1, Th4, CARD_1:49, TARSKI:def 1
.= op2 . (x,y) by CARD_1:49, FUNCOP_1:77 ; :: thesis: verum

end;

hence SymGroup {} = Trivial-multMagma by A1, Th4, BINOP_1:2; :: thesis: verum