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
now :: thesis: for j being Nat st j in Seg (len G) holds
f . 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;
hence f = g by FINSEQ_2:119; :: thesis: verum