let x, y be non empty homogeneous quasi_total PartFunc of ([:A,B:] *),[:A,B:]; :: thesis: ( dom x = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom x holds
x . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) & dom y = (arity f1) -tuples_on [:A,B:] & ( for h being FinSequence of [:A,B:] st h in dom y holds
y . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ) implies x = y )
assume that
A25: dom x = (arity f1) -tuples_on [:A,B:] and
A26: for h being FinSequence of [:A,B:] st h in dom x holds
x . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] and
A27: dom y = (arity f1) -tuples_on [:A,B:] and
A28: for h being FinSequence of [:A,B:] st h in dom y holds
y . h = [(f1 . (pr1 h)),(f2 . (pr2 h))] ; :: thesis: x = y
now :: thesis: for c being Element of [:A,B:] * st c in dom x holds
x . c = y . c
let c be Element of [:A,B:] * ; :: thesis: ( c in dom x implies x . c = y . c )
reconsider c9 = c as FinSequence of [:A,B:] ;
assume A29: c in dom x ; :: thesis: x . c = y . c
then x . c9 = [(f1 . (pr1 c9)),(f2 . (pr2 c9))] by A26;
hence x . c = y . c by A25, A27, A28, A29; :: thesis: verum
end;
hence x = y by A25, A27, PARTFUN1:5; :: thesis: verum