let X be set ; :: thesis: for G being non empty multMagma
for f, g being Element of (.: G,X) st ( for x being set 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 set st x in X holds
f . x = g . x ) holds
f = g
let f, g be Element of (.: G,X); :: thesis: ( ( for x being set st x in X holds
f . x = g . x ) implies f = g )
( dom f = X & dom g = X ) by Th20;
hence ( ( for x being set st x in X holds
f . x = g . x ) implies f = g ) by FUNCT_1:9; :: thesis: verum