let a, b be object ; <*a,b*> = (1,2) --> (a,b)
set f = (1,2) --> (a,b);
set g = <*a,b*>;
A1:
dom ((1,2) --> (a,b)) = {1,2}
by FUNCT_4:62;
A2:
now for x being object st x in dom ((1,2) --> (a,b)) holds
((1,2) --> (a,b)) . x = <*a,b*> . xlet x be
object ;
( x in dom ((1,2) --> (a,b)) implies ((1,2) --> (a,b)) . b1 = <*a,b*> . b1 )assume A3:
x in dom ((1,2) --> (a,b))
;
((1,2) --> (a,b)) . b1 = <*a,b*> . b1 end;
dom <*a,b*> = {1,2}
by FINSEQ_1:2, FINSEQ_1:89;
hence
<*a,b*> = (1,2) --> (a,b)
by A2, FUNCT_1:2, FUNCT_4:62; verum