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

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