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)) . b1 = <*a,b*> . b1 )
assume A3: x in dom ((1,2) --> (a,b)) ; :: thesis: ((1,2) --> (a,b)) . b1 = <*a,b*> . b1
per cases ( x = 1 or x = 2 ) by A1, A3, TARSKI:def 2;
suppose A4: x = 1 ; :: thesis: ((1,2) --> (a,b)) . b1 = <*a,b*> . b1
hence ((1,2) --> (a,b)) . x = a by FUNCT_4:63
.= <*a,b*> . x by A4, FINSEQ_1:44 ;
:: thesis: verum
end;
suppose A5: x = 2 ; :: thesis: ((1,2) --> (a,b)) . b1 = <*a,b*> . b1
hence ((1,2) --> (a,b)) . x = b by FUNCT_4:63
.= <*a,b*> . x by A5, FINSEQ_1:44 ;
:: 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