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
A23: dom F = (arity o) -tuples_on (Class E) and
A24: 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
A25: dom G = (arity o) -tuples_on (Class E) and
A26: 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 object st a in dom F holds
F . a = G . a

proof

let a be object ; :: 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 FINSEQ_3:122;
F . b = Class (E,(o . x)) by A24, A27, A28;
hence F . a = G . a by A23, A25, A26, A27, A28; :: thesis: verum

end;

hence F = G by A23, A25; :: thesis: verum