let X be set ; :: thesis: for G being non empty multMagma

for f, g being Element of (.: (G,X)) st ( for x being object st x in X holds

f . x = g . x ) holds

f = g

let G be non empty multMagma ; :: thesis: for f, g being Element of (.: (G,X)) st ( for x being object st x in X holds

f . x = g . x ) holds

f = g

let f, g be Element of (.: (G,X)); :: thesis: ( ( for x being object st x in X holds

f . x = g . x ) implies f = g )

( dom f = X & dom g = X ) by Th19;

hence ( ( for x being object st x in X holds

f . x = g . x ) implies f = g ) by FUNCT_1:2; :: thesis: verum

for f, g being Element of (.: (G,X)) st ( for x being object st x in X holds

f . x = g . x ) holds

f = g

let G be non empty multMagma ; :: thesis: for f, g being Element of (.: (G,X)) st ( for x being object st x in X holds

f . x = g . x ) holds

f = g

let f, g be Element of (.: (G,X)); :: thesis: ( ( for x being object st x in X holds

f . x = g . x ) implies f = g )

( dom f = X & dom g = X ) by Th19;

hence ( ( for x being object st x in X holds

f . x = g . x ) implies f = g ) by FUNCT_1:2; :: thesis: verum