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