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:
set h = SymGroupsIso p;
A2: rng p = Y by ;
reconsider p1 = p " as Function of Y,X by ;
A3: id X = p1 * p by ;
let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom () or not y in dom () or not () . x = () . y or x = y )
assume that
A4: ( x in dom () & y in dom () ) and
A5: (SymGroupsIso p) . x = () . y ; :: thesis: x = y
reconsider x = x, y = y as Element of () by A4;
reconsider f = x, g = y as Permutation of X by Th5;
( (SymGroupsIso p) . x = (p * f) * p1 & () . y = (p * g) * p1 ) by ;
then (p * f) * (p1 * p) = ((p * g) * p1) * p by ;
then (p * f) * (p1 * p) = (p * g) * (p1 * p) by RELAT_1:36;
then p * f = (p * g) * (id X) by ;
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 ;
hence x = y by FUNCT_2:17; :: thesis: verum