let it1, it2 be FinSequence of the carrier of L; :: thesis: ( dom it1 = dom F & ( for i being Nat st i in dom F holds
it1 . i = eval ((~ (F /. i)),x) ) & dom it2 = dom F & ( for i being Nat st i in dom F holds
it2 . i = eval ((~ (F /. i)),x) ) implies it1 = it2 )
assume that
A3: dom it1 = dom F and
A4: for i being Nat st i in dom F holds
it1 . i = eval ((~ (F /. i)),x) and
A5: dom it2 = dom F and
A6: for i being Nat st i in dom F holds
it2 . i = eval ((~ (F /. i)),x) ; :: thesis: it1 = it2
for n being Nat st n in dom it1 holds
it1 . n = it2 . n

proof

let n be Nat; :: thesis: ( n in dom it1 implies it1 . n = it2 . n )
assume A7: n in dom it1 ; :: thesis: it1 . n = it2 . n
reconsider n = n as Element of NAT by ORDINAL1:def 12;
it1 . n = eval ((~ (F /. n)),x) by A3, A4, A7
.= it2 . n by A3, A6, A7 ;
hence it1 . n = it2 . n ; :: thesis: verum

end;

hence it1 = it2 by A3, A5; :: thesis: verum