let f1, f2 be Function of [:[: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:],[: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:]:],REAL; :: thesis: ( ( for x1, y1 being Element of X

for x2, y2 being Element of Y

for x3, y3 being Element of Z

for x4, y4 being Element of W

for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:] st x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] holds

f1 . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + ((dist (x3,y3)) + (dist (x4,y4))) ) & ( for x1, y1 being Element of X

for x2, y2 being Element of Y

for x3, y3 being Element of Z

for x4, y4 being Element of W

for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:] st x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] holds

f2 . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + ((dist (x3,y3)) + (dist (x4,y4))) ) implies f1 = f2 )

assume that

A2: for x1, y1 being Element of X

for x2, y2 being Element of Y

for x3, y3 being Element of Z

for x4, y4 being Element of W

for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:] st x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] holds

f1 . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + ((dist (x3,y3)) + (dist (x4,y4))) and

A3: for x1, y1 being Element of X

for x2, y2 being Element of Y

for x3, y3 being Element of Z

for x4, y4 being Element of W

for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:] st x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] holds

f2 . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + ((dist (x3,y3)) + (dist (x4,y4))) ; :: thesis: f1 = f2

for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:] holds f1 . (x,y) = f2 . (x,y)

for x2, y2 being Element of Y

for x3, y3 being Element of Z

for x4, y4 being Element of W

for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:] st x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] holds

f1 . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + ((dist (x3,y3)) + (dist (x4,y4))) ) & ( for x1, y1 being Element of X

for x2, y2 being Element of Y

for x3, y3 being Element of Z

for x4, y4 being Element of W

for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:] st x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] holds

f2 . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + ((dist (x3,y3)) + (dist (x4,y4))) ) implies f1 = f2 )

assume that

A2: for x1, y1 being Element of X

for x2, y2 being Element of Y

for x3, y3 being Element of Z

for x4, y4 being Element of W

for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:] st x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] holds

f1 . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + ((dist (x3,y3)) + (dist (x4,y4))) and

A3: for x1, y1 being Element of X

for x2, y2 being Element of Y

for x3, y3 being Element of Z

for x4, y4 being Element of W

for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:] st x = [x1,x2,x3,x4] & y = [y1,y2,y3,y4] holds

f2 . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + ((dist (x3,y3)) + (dist (x4,y4))) ; :: thesis: f1 = f2

for x, y being Element of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:] holds f1 . (x,y) = f2 . (x,y)

proof

hence
f1 = f2
by BINOP_1:2; :: thesis: verum
let x, y be Element of [: the carrier of X, the carrier of Y, the carrier of Z, the carrier of W:]; :: thesis: f1 . (x,y) = f2 . (x,y)

consider x1 being Element of X, x2 being Element of Y, x3 being Element of Z, x4 being Element of W such that

A4: x = [x1,x2,x3,x4] by DOMAIN_1:10;

consider y1 being Element of X, y2 being Element of Y, y3 being Element of Z, y4 being Element of W such that

A5: y = [y1,y2,y3,y4] by DOMAIN_1:10;

thus f1 . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + ((dist (x3,y3)) + (dist (x4,y4))) by A2, A4, A5

.= f2 . (x,y) by A3, A4, A5 ; :: thesis: verum

end;consider x1 being Element of X, x2 being Element of Y, x3 being Element of Z, x4 being Element of W such that

A4: x = [x1,x2,x3,x4] by DOMAIN_1:10;

consider y1 being Element of X, y2 being Element of Y, y3 being Element of Z, y4 being Element of W such that

A5: y = [y1,y2,y3,y4] by DOMAIN_1:10;

thus f1 . (x,y) = ((dist (x1,y1)) + (dist (x2,y2))) + ((dist (x3,y3)) + (dist (x4,y4))) by A2, A4, A5

.= f2 . (x,y) by A3, A4, A5 ; :: thesis: verum