let F, G be non empty homogeneous quasi_total PartFunc of ((Class E) * ),(Class E); :: thesis: ( dom F = (arity o) -tuples_on (Class E) & ( for y being FinSequence of Class E st y in dom F holds
for x being FinSequence of the carrier of U1 st x is_representatives_FS y holds
F . y = Class E,(o . x) ) & dom G = (arity o) -tuples_on (Class E) & ( for y being FinSequence of Class E st y in dom G holds
for x being FinSequence of the carrier of U1 st x is_representatives_FS y holds
G . y = Class E,(o . x) ) implies F = G )
assume that
A25: ( dom F = (arity o) -tuples_on (Class E) & ( for y being FinSequence of Class E st y in dom F holds
for x being FinSequence of the carrier of U1 st x is_representatives_FS y holds
F . y = Class E,(o . x) ) ) and
A26: ( dom G = (arity o) -tuples_on (Class E) & ( for y being FinSequence of Class E st y in dom G holds
for x being FinSequence of the carrier of U1 st x is_representatives_FS y holds
G . y = Class E,(o . x) ) ) ; :: thesis: F = G
for a being set st a in dom F holds
F . a = G . a

proof

let a be set ; :: thesis: ( a in dom F implies F . a = G . a )
assume A27: a in dom F ; :: thesis: F . a = G . a
then reconsider b = a as FinSequence of Class E by FINSEQ_1:def 11;
consider x being FinSequence of the carrier of U1 such that
A28: x is_representatives_FS b by Th19;
( F . b = Class E,(o . x) & G . b = Class E,(o . x) ) by A25, A26, A27, A28;
hence F . a = G . a ; :: thesis: verum

end;

hence F = G by A25, A26, FUNCT_1:9; :: thesis: verum