let a, b, c be object ; :: thesis: <*a,b,c*> = (1,2,3) --> (a,b,c)
set f = (1,2,3) --> (a,b,c);
set g = <*a,b,c*>;
A1: dom <*a,b,c*> = Seg (len <*a,b,c*>) by FINSEQ_1:def 3
.= {1,2,3} by FINSEQ_1:45, FINSEQ_3:1 ;
A2: dom ((1,2,3) --> (a,b,c)) = {1,2,3} by FUNCT_4:128;
now :: thesis: for x being object st x in dom ((1,2,3) --> (a,b,c)) holds
((1,2,3) --> (a,b,c)) . x = <*a,b,c*> . x
let x be object ; :: thesis: ( x in dom ((1,2,3) --> (a,b,c)) implies ((1,2,3) --> (a,b,c)) . b1 = <*a,b,c*> . b1 )
assume A3: x in dom ((1,2,3) --> (a,b,c)) ; :: thesis: ((1,2,3) --> (a,b,c)) . b1 = <*a,b,c*> . b1
per cases ( x = 1 or x = 2 or x = 3 ) by A2, A3, ENUMSET1:def 1;
suppose A4: x = 1 ; :: thesis: ((1,2,3) --> (a,b,c)) . b1 = <*a,b,c*> . b1
hence ((1,2,3) --> (a,b,c)) . x = a by FUNCT_4:134
.= <*a,b,c*> . x by A4, FINSEQ_1:45 ;
:: thesis: verum
end;
suppose A5: x = 2 ; :: thesis: ((1,2,3) --> (a,b,c)) . b1 = <*a,b,c*> . b1
hence ((1,2,3) --> (a,b,c)) . x = b by FUNCT_4:135
.= <*a,b,c*> . x by A5, FINSEQ_1:45 ;
:: thesis: verum
end;
suppose A6: x = 3 ; :: thesis: ((1,2,3) --> (a,b,c)) . b1 = <*a,b,c*> . b1
hence ((1,2,3) --> (a,b,c)) . x = c by FUNCT_4:135
.= <*a,b,c*> . x by A6, FINSEQ_1:45 ;
:: thesis: verum
end;
end;
end;
hence <*a,b,c*> = (1,2,3) --> (a,b,c) by A1, FUNCT_4:128, FUNCT_1:2; :: thesis: verum