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