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

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