let X, Y be non empty set ; :: thesis: for p being Function of X,Y st p is bijective holds

SymGroupsIso p is multiplicative

let p be Function of X,Y; :: thesis: ( p is bijective implies SymGroupsIso p is multiplicative )

assume A1: p is bijective ; :: thesis: 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); :: according to GROUP_6:def 6 :: thesis: (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 ; :: thesis: verum

SymGroupsIso p is multiplicative

let p be Function of X,Y; :: thesis: ( p is bijective implies SymGroupsIso p is multiplicative )

assume A1: p is bijective ; :: thesis: 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); :: according to GROUP_6:def 6 :: thesis: (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 ; :: thesis: verum