let D be ManySortedSet of NAT ; :: thesis: ( (Product_dom D) . 0 = D . 0 & (Product_dom D) . 1 = [:(D . 0),(D . 1):] & (Product_dom D) . 2 = [:(D . 0),(D . 1),(D . 2):] & (Product_dom D) . 3 = [:(D . 0),(D . 1),(D . 2),(D . 3):] )
thus (Product_dom D) . 0 = D . 0 by Def10; :: thesis: ( (Product_dom D) . 1 = [:(D . 0),(D . 1):] & (Product_dom D) . 2 = [:(D . 0),(D . 1),(D . 2):] & (Product_dom D) . 3 = [:(D . 0),(D . 1),(D . 2),(D . 3):] )
thus A1: (Product_dom D) . 1 = (Product_dom D) . (0 + 1)
.= [:((Product_dom D) . 0),(D . 1):] by Def10
.= [:(D . 0),(D . 1):] by Def10 ; :: thesis: ( (Product_dom D) . 2 = [:(D . 0),(D . 1),(D . 2):] & (Product_dom D) . 3 = [:(D . 0),(D . 1),(D . 2),(D . 3):] )
thus A2: (Product_dom D) . 2 = [:((Product_dom D) . 1),(D . (1 + 1)):] by Def10
.= [:(D . 0),(D . 1),(D . 2):] by ZFMISC_1:def 3, A1 ; :: thesis: (Product_dom D) . 3 = [:(D . 0),(D . 1),(D . 2),(D . 3):]
thus (Product_dom D) . 3 = [:((Product_dom D) . 2),(D . (2 + 1)):] by Def10
.= [:(D . 0),(D . 1),(D . 2),(D . 3):] by ZFMISC_1:def 4, A2 ; :: thesis: verum