let F, G be PFuncFinSequence of (Class E); :: thesis: ( len F = len the charact of U1 & ( for n being 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 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 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 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 :: thesis: for n being Nat st n in dom F holds
F . n = G . n
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 3;
A8: ( dom F = dom the charact of U1 & dom G = dom the charact of U1 ) by A3, A5, FINSEQ_3:29;
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:9; :: thesis: verum