let G, H be UnOp of (n -tuples_on D); :: thesis: ( ( for x being Element of n -tuples_on D holds G . x = F * x ) & ( for x being Element of n -tuples_on D holds H . x = F * x ) implies G = H )

assume that

A3: for x being Element of n -tuples_on D holds G . x = F * x and

A4: for x being Element of n -tuples_on D holds H . x = F * x ; :: thesis: G = H

assume that

A3: for x being Element of n -tuples_on D holds G . x = F * x and

A4: for x being Element of n -tuples_on D holds H . x = F * x ; :: thesis: G = H

now :: thesis: for x being Element of n -tuples_on D holds G . x = H . x

hence
G = H
by FUNCT_2:63; :: thesis: verumlet x be Element of n -tuples_on D; :: thesis: G . x = H . x

G . x = F * x by A3;

hence G . x = H . x by A4; :: thesis: verum

end;G . x = F * x by A3;

hence G . x = H . x by A4; :: thesis: verum