let a, b be object ; :: thesis: <*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 :: thesis: for x being object st x in dom ((1,2) --> (a,b)) holds
((1,2) --> (a,b)) . x = <*a,b*> . x

let x be object ; :: thesis: ( x in dom ((1,2) --> (a,b)) implies ((1,2) --> (a,b)) . b₁ = <*a,b*> . b₁ )
assume A3: x in dom ((1,2) --> (a,b)) ; :: thesis: ((1,2) --> (a,b)) . b₁ = <*a,b*> . b₁

per cases ( x = 1 or x = 2 ) by A1, A3, TARSKI:def 2;

suppose A4: x = 1 ; :: thesis: ((1,2) --> (a,b)) . b₁ = <*a,b*> . b₁

hence ((1,2) --> (a,b)) . x = a by FUNCT_4:63
.= <*a,b*> . x by A4 ;
:: thesis: verum

end;

suppose A5: x = 2 ; :: thesis: ((1,2) --> (a,b)) . b₁ = <*a,b*> . b₁

hence ((1,2) --> (a,b)) . x = b by FUNCT_4:63
.= <*a,b*> . x by A5 ;
:: thesis: verum

end;

end;

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; :: thesis: verum