let X, Y be non empty set ; :: thesis: for p being Function of X,Y st p is bijective holds
SymGroupsIso p is one-to-one
let p be Function of X,Y; :: thesis: ( p is bijective implies SymGroupsIso p is one-to-one )
assume A1: p is bijective ; :: thesis: SymGroupsIso p is one-to-one
set h = SymGroupsIso p;
A2: rng p = Y by A1, FUNCT_2:def 3;
reconsider p1 = p " as Function of Y,X by A1, A2, FUNCT_2:25;
A3: id X = p1 * p by A1, A2, FUNCT_2:29;
let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom (SymGroupsIso p) or not y in dom (SymGroupsIso p) or not (SymGroupsIso p) . x = (SymGroupsIso p) . y or x = y )
assume that
A4: ( x in dom (SymGroupsIso p) & y in dom (SymGroupsIso p) ) and
A5: (SymGroupsIso p) . x = (SymGroupsIso p) . y ; :: thesis: x = y
reconsider x = x, y = y as Element of (SymGroup X) by A4;
reconsider f = x, g = y as Permutation of X by Th5;
( (SymGroupsIso p) . x = (p * f) * p1 & (SymGroupsIso p) . y = (p * g) * p1 ) by A1, Def3;
then (p * f) * (p1 * p) = ((p * g) * p1) * p by A5, RELAT_1:36;
then (p * f) * (p1 * p) = (p * g) * (p1 * p) by RELAT_1:36;
then p * f = (p * g) * (id X) by A3, FUNCT_2:17;
then p1 * (p * f) = p1 * (p * g) by FUNCT_2:17;
then (p1 * p) * f = p1 * (p * g) by RELAT_1:36;
then (p1 * p) * f = (p1 * p) * g by RELAT_1:36;
then f = (id X) * g by A3, FUNCT_2:17;
hence x = y by FUNCT_2:17; :: thesis: verum