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

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

let 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;

hence G = H by FUNCT_2:63; :: thesis: verum