let p1, p2 be PFuncFinSequence of A; :: thesis: ( dom p1 = dom the charact of U0 & ( for n being set
for o being operation of U0 st n in dom p1 & o = the charact of U0 . n holds
p1 . n = o /. A ) & dom p2 = dom the charact of U0 & ( for n being set
for o being operation of U0 st n in dom p2 & o = the charact of U0 . n holds
p2 . n = o /. A ) implies p1 = p2 )
assume A5: ( dom p1 = dom the charact of U0 & ( for n being set
for o being operation of U0 st n in dom p1 & o = the charact of U0 . n holds
p1 . n = o /. A ) & dom p2 = dom the charact of U0 & ( for n being set
for o being operation of U0 st n in dom p2 & o = the charact of U0 . n holds
p2 . n = o /. A ) ) ; :: thesis: p1 = p2
for n being Nat st n in dom the charact of U0 holds
p1 . n = p2 . n

proof

let n be Nat; :: thesis: ( n in dom the charact of U0 implies p1 . n = p2 . n )
assume A6: n in dom the charact of U0 ; :: thesis: p1 . n = p2 . n
then reconsider k = the charact of U0 . n as operation of U0 by FUNCT_1:def 5;
( p1 . n = k /. A & p2 . n = k /. A ) by A5, A6;
hence p1 . n = p2 . n ; :: thesis: verum

end;

hence p1 = p2 by A5, FINSEQ_1:17; :: thesis: verum