consider D being disjoint_with_NAT set ;
consider f being non empty with_zero FinSequence of NAT ;
take FreeUnivAlgZAO (f,D) ; :: thesis: ( FreeUnivAlgZAO (f,D) is strict & FreeUnivAlgZAO (f,D) is free & FreeUnivAlgZAO (f,D) is with_const_op )
thus ( FreeUnivAlgZAO (f,D) is strict & FreeUnivAlgZAO (f,D) is free & FreeUnivAlgZAO (f,D) is with_const_op ) by Th8; :: thesis: verum