let f, g be Element of REAL (len G); :: thesis: ( len f = len G & ( for j being Element of dom G holds f . j = the normF of (G . j) . (x . j) ) & len g = len G & ( for j being Element of dom G holds g . j = the normF of (G . j) . (x . j) ) implies f = g )

assume that

len f = len G and

A5: for j being Element of dom G holds f . j = the normF of (G . j) . (x . j) and

len g = len G and

A6: for j being Element of dom G holds g . j = the normF of (G . j) . (x . j) ; :: thesis: f = g

assume that

len f = len G and

A5: for j being Element of dom G holds f . j = the normF of (G . j) . (x . j) and

len g = len G and

A6: for j being Element of dom G holds g . j = the normF of (G . j) . (x . j) ; :: thesis: f = g

now :: thesis: for j being Nat st j in Seg (len G) holds

f . j = g . j

hence
f = g
by FINSEQ_2:119; :: thesis: verumf . j = g . j

let j be Nat; :: thesis: ( j in Seg (len G) implies f . j = g . j )

assume j in Seg (len G) ; :: thesis: f . j = g . j

then reconsider j1 = j as Element of dom G by FINSEQ_1:def 3;

f . j = the normF of (G . j1) . (x . j1) by A5;

hence f . j = g . j by A6; :: thesis: verum

end;assume j in Seg (len G) ; :: thesis: f . j = g . j

then reconsider j1 = j as Element of dom G by FINSEQ_1:def 3;

f . j = the normF of (G . j1) . (x . j1) by A5;

hence f . j = g . j by A6; :: thesis: verum