let a, b be set ; :: 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:65;

A2: now

let x be set ; :: 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:66
.= <*a,b*> . x by A4, FINSEQ_1:61 ;
:: 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:66
.= <*a,b*> . x by A5, FINSEQ_1:61 ;
:: thesis: verum

end;

end;

end;

dom <*a,b*> = {1,2} by FINSEQ_1:4, FINSEQ_3:29;
hence <*a,b*> = 1,2 --> a,b by A2, FUNCT_1:9, FUNCT_4:65; :: thesis: verum