let F, G be PFuncFinSequence of (Class E); :: thesis: ( len F = len the charact of U1 & ( for n being Element of NAT st n in dom F holds
for o1 being operation of U1 st the charact of U1 . n = o1 holds
F . n = QuotOp o1,E ) & len G = len the charact of U1 & ( for n being Element of NAT st n in dom G holds
for o1 being operation of U1 st the charact of U1 . n = o1 holds
G . n = QuotOp o1,E ) implies F = G )
assume that
A3: ( len F = len the charact of U1 & ( for n being Element of NAT st n in dom F holds
for o1 being operation of U1 st the charact of U1 . n = o1 holds
F . n = QuotOp o1,E ) ) and
A4: ( len G = len the charact of U1 & ( for n being Element of NAT st n in dom G holds
for o1 being operation of U1 st the charact of U1 . n = o1 holds
G . n = QuotOp o1,E ) ) ; :: thesis: F = G

now

A5: ( dom F = dom the charact of U1 & Seg (len F) = dom the charact of U1 & dom G = dom the charact of U1 & Seg (len G) = dom the charact of U1 & dom F = Seg (len the charact of U1) & dom G = Seg (len the charact of U1) ) by A3, A4, FINSEQ_1:def 3, FINSEQ_3:31;
X: dom F = Seg (len the charact of U1) by A3, FINSEQ_1:def 3;
let n be Nat; :: thesis: ( n in dom F implies F . n = G . n )
assume A6: n in dom F ; :: thesis: F . n = G . n
then n in dom the charact of U1 by FINSEQ_1:def 3, X;
then reconsider o1 = the charact of U1 . n as operation of U1 by FUNCT_1:def 5;
( F . n = QuotOp o1,E & G . n = QuotOp o1,E ) by A3, A4, A5, A6;
hence F . n = G . n ; :: thesis: verum

end;

hence F = G by A3, A4, FINSEQ_2:10; :: thesis: verum