let I, J be non empty set ; :: thesis: for a being Function of I,J
for x, y being Function st dom x = I & dom y = J & a is bijective holds
( x = y * a iff y = x * (a ") )
let a be Function of I,J; :: thesis: for x, y being Function st dom x = I & dom y = J & a is bijective holds
( x = y * a iff y = x * (a ") )
let x, y be Function; :: thesis: ( dom x = I & dom y = J & a is bijective implies ( x = y * a iff y = x * (a ") ) )
assume that
A1: dom x = I and
A2: dom y = J and
A3: a is bijective ; :: thesis: ( x = y * a iff y = x * (a ") )
A4: ( dom a = I & rng a = J ) by A3, GROUP_6:61;

hereby :: thesis: ( y = x * (a ") implies x = y * a )

assume A5: x = y * a ; :: thesis: y = x * (a ")
thus y = y * (id J) by A2, RELAT_1:51
.= y * (a * (a ")) by A3, A4, FUNCT_2:29
.= x * (a ") by A5, RELAT_1:36 ; :: thesis: verum

end;

assume A6: y = x * (a ") ; :: thesis: x = y * a
thus x = x * (id I) by A1, RELAT_1:51
.= x * ((a ") * a) by A3, A4, FUNCT_2:29
.= y * a by A6, RELAT_1:36 ; :: thesis: verum