let x1, x2 be object ; :: thesis: <*x1,x2*> = {[1,x1],[2,x2]}
reconsider f = {[1,x1],[2,x2]} as Function by GRFUNC_1:8;
A1: dom f = {1,2} by RELAT_1:10;
then A2: dom <*x1,x2*> = dom f by Th2, Th88;

now :: thesis: for x being object st x in {1,2} holds
f . x = <*x1,x2*> . x

let x be object ; :: 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 ;
[x,x1] in f by A4, TARSKI:def 2;
hence f . x = <*x1,x2*> . x by A5, FUNCT_1:1; :: thesis: verum

end;

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

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

end;

end;

end;

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