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 and
A4: 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
A5: len G = len the charact of U1 and
A6: 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

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

end;

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