let f, g be Function of (SymGroup X),(SymGroup Y); :: thesis: ( ( for x being Element of (SymGroup X) holds f . x = (p * x) * (p ") ) & ( for x being Element of (SymGroup X) holds g . x = (p * x) * (p ") ) implies f = g )
assume that
A7: for x being Element of (SymGroup X) holds f . x = (p * x) * (p ") and
A8: for x being Element of (SymGroup X) holds g . x = (p * x) * (p ") ; :: thesis: f = g
let x be Element of (SymGroup X); :: according to FUNCT_2:def 8 :: thesis: f . x = g . x
thus f . x = (p * x) * (p ") by A7
.= g . x by A8 ; :: thesis: verum