let x1, x2 be set ; :: thesis: <*x1,x2*> = {[1,x1],[2,x2]}
reconsider f = {[1,x1],[2,x2]} as Function by GRFUNC_1:19;
A1: dom f = {1,2} by RELAT_1:24;
then A2: dom <*x1,x2*> = dom f by FINSEQ_1:4, FINSEQ_3:29;

now

let x be set ; :: thesis: ( x in {1,2} implies f . b₁ = <*x1,x2*> . b₁ )
assume A3: x in {1,2} ; :: thesis: f . b₁ = <*x1,x2*> . b₁

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

suppose A4: x = 1 ; :: thesis: f . b₁ = <*x1,x2*> . b₁

then A5: <*x1,x2*> . x = x1 by FINSEQ_1:61;
[x,x1] in f by A4, TARSKI:def 2;
hence f . x = <*x1,x2*> . x by A5, FUNCT_1:8; :: thesis: verum

end;

suppose A6: x = 2 ; :: thesis: f . b₁ = <*x1,x2*> . b₁

then A7: <*x1,x2*> . x = x2 by FINSEQ_1:61;
[x,x2] in f by A6, TARSKI:def 2;
hence f . x = <*x1,x2*> . x by A7, FUNCT_1:8; :: thesis: verum

end;

end;

end;

hence <*x1,x2*> = {[1,x1],[2,x2]} by A1, A2, FUNCT_1:9; :: thesis: verum