let A be non empty set ; :: thesis: for f, g being Permutation of A holds (f ") \ g = (f \ g) "

let f, g be Permutation of A; :: thesis: (f ") \ g = (f \ g) "

thus (f \ g) " = ((g ") ") * ((g * f) ") by FUNCT_1:44

.= ((g ") ") * ((f ") * (g ")) by FUNCT_1:44

.= g * ((f ") * (g ")) by FUNCT_1:43

.= (f ") \ g by RELAT_1:36 ; :: thesis: verum

let f, g be Permutation of A; :: thesis: (f ") \ g = (f \ g) "

thus (f \ g) " = ((g ") ") * ((g * f) ") by FUNCT_1:44

.= ((g ") ") * ((f ") * (g ")) by FUNCT_1:44

.= g * ((f ") * (g ")) by FUNCT_1:43

.= (f ") \ g by RELAT_1:36 ; :: thesis: verum