let A be non empty set ; :: thesis: for a being Element of A
for f, g being Permutation of A st f . a = a holds
(f \ g) . (g . a) = g . a
let a be Element of A; :: thesis: for f, g being Permutation of A st f . a = a holds
(f \ g) . (g . a) = g . a
let f, g be Permutation of A; :: thesis: ( f . a = a implies (f \ g) . (g . a) = g . a )
assume A1: f . a = a ; :: thesis: (f \ g) . (g . a) = g . a
(g ") . (g . a) = ((g ") * g) . a by FUNCT_2:15
.= (id A) . a by FUNCT_2:61
.= a ;
hence (f \ g) . (g . a) = (g * f) . a by FUNCT_2:15
.= g . a by A1, FUNCT_2:15 ;
:: thesis: verum