let S be 1-sorted ; :: thesis: Carrier <*S*> = <* the carrier of S*>
thus Carrier <*S*> = Carrier {[1,S]} by FINSEQ_1:def 5
.= Carrier (1 .--> S) by FUNCT_4:82
.= Carrier ({1} --> S)
.= {1} --> the carrier of S by Th15
.= 1 .--> the carrier of S
.= {[1, the carrier of S]} by FUNCT_4:82
.= <* the carrier of S*> by FINSEQ_1:def 5 ; :: thesis: verum