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