let a, b be Function of G,(SymGroup the carrier of G); :: thesis: ( ( for g being Element of G holds a . g = * g ) & ( for g being Element of G holds b . g = * g ) implies a = b )
assume that
A2: for g being Element of G holds a . g = * g and
A3: for g being Element of G holds b . g = * g ; :: thesis: a = b
let x be Element of G; :: according to FUNCT_2:def 8 :: thesis: a . x = b . x
thus a . x = * x by A2
.= b . x by A3 ; :: thesis: verum