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
A22: dom F = (arity o) -tuples_on (Class E) and
A23: 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
A24: dom G = (arity o) -tuples_on (Class E) and
A25: 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 A26: 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
A27: x is_representatives_FS b by FINSEQ_3:131;
F . b = Class E,(o . x) by A23, A26, A27;
hence F . a = G . a by A22, A24, A25, A26, A27; :: thesis: verum

end;

hence F = G by A22, A24, FUNCT_1:9; :: thesis: verum