set G = SymGroup {};

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

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)

hence
SymGroup {} = Trivial-multMagma
by A1, Th4, BINOP_1:2; :: thesis: verumlet 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;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