set G = SymGroup {};
A1: the carrier of (SymGroup {}) = permutations {} by Def2;
now :: thesis: for x, y being Element of {{}} holds the multF of (SymGroup {}) . (x,y) = op2 . (x,y)
let x, y be Element of {{}}; :: 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, TARSKI:def 1
.= op2 . (x,y) by FUNCOP_1:77 ; :: thesis: verum
end;
hence SymGroup {} = Trivial-multMagma by A1, Th4, BINOP_1:2; :: thesis: verum