consider f being non empty with_zero FinSequence of NAT ;
consider D being disjoint_with_NAT set ;
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