let x1, x2 be set ; :: 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 . b1 = <*x1,x2*> . b1 )
assume A3: x in {1,2} ; :: thesis: f . b1 = <*x1,x2*> . b1
per cases ( x = 1 or x = 2 ) by A3, TARSKI:def 2;
suppose A4: x = 1 ; :: thesis: f . b1 = <*x1,x2*> . b1
then A5: <*x1,x2*> . x = x1 by Th44;
[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 . b1 = <*x1,x2*> . b1
then A7: <*x1,x2*> . x = x2 by Th44;
[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