let n, m be Nat; :: thesis: for Y being ref-finite ConstructorDB

for B being FinSequence of the Constrs of Y holds EXACTLY B c= EXACTLY+- (B,n,m)

let Y be ref-finite ConstructorDB ; :: thesis: for B being FinSequence of the Constrs of Y holds EXACTLY B c= EXACTLY+- (B,n,m)

let B be FinSequence of the Constrs of Y; :: thesis: EXACTLY B c= EXACTLY+- (B,n,m)

( EXACTLY B = EXACTLY+- (B,0,0) & 0 <= n & 0 <= m ) by Th69, NAT_1:2;

hence EXACTLY B c= EXACTLY+- (B,n,m) by Th72; :: thesis: verum

for B being FinSequence of the Constrs of Y holds EXACTLY B c= EXACTLY+- (B,n,m)

let Y be ref-finite ConstructorDB ; :: thesis: for B being FinSequence of the Constrs of Y holds EXACTLY B c= EXACTLY+- (B,n,m)

let B be FinSequence of the Constrs of Y; :: thesis: EXACTLY B c= EXACTLY+- (B,n,m)

( EXACTLY B = EXACTLY+- (B,0,0) & 0 <= n & 0 <= m ) by Th69, NAT_1:2;

hence EXACTLY B c= EXACTLY+- (B,n,m) by Th72; :: thesis: verum