let X, Y be non empty set ; for p being Function of X,Y st p is bijective holds
SymGroupsIso p is multiplicative
let p be Function of X,Y; ( p is bijective implies SymGroupsIso p is multiplicative )
assume A1:
p is bijective
; SymGroupsIso p is multiplicative
set h = SymGroupsIso p;
A2:
rng p = Y
by A1, FUNCT_2:def 3;
let x, y be Element of (SymGroup X); GROUP_6:def 6 (SymGroupsIso p) . (x * y) = ((SymGroupsIso p) . x) * ((SymGroupsIso p) . y)
reconsider p1 = p " as Function of Y,X by A1, A2, FUNCT_2:25;
A3:
id X = p1 * p
by A2, A1, FUNCT_2:29;
A4:
( (SymGroupsIso p) . x = (p * x) * p1 & (SymGroupsIso p) . y = (p * y) * p1 )
by A1, Def3;
reconsider f = x, g = y as Permutation of X by Th5;
thus (SymGroupsIso p) . (x * y) =
(p * (x * y)) * p1
by A1, Def3
.=
(p * (g * f)) * p1
by Def2
.=
(p * ((g * (id X)) * f)) * p1
by FUNCT_2:17
.=
(p * (((g * p1) * p) * f)) * p1
by A3, RELAT_1:36
.=
(p * ((g * p1) * (p * f))) * p1
by RELAT_1:36
.=
((p * (g * p1)) * (p * f)) * p1
by RELAT_1:36
.=
(p * (g * p1)) * ((p * f) * p1)
by RELAT_1:36
.=
((p * g) * p1) * ((p * f) * p1)
by RELAT_1:36
.=
((SymGroupsIso p) . x) * ((SymGroupsIso p) . y)
by A4, Def2
; verum