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

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