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

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