set A = the non empty set ;
set char = the non-empty non empty homogeneous quasi_total PFuncFinSequence of the non empty set ;
set assign = the Function of (Union [|X, the Sorts of T|]), the non empty set ;
take P = ProgramAlgStr(# the non empty set , the non-empty non empty homogeneous quasi_total PFuncFinSequence of the non empty set , the Function of (Union [|X, the Sorts of T|]), the non empty set #); :: thesis: ( P is partial & P is quasi_total & P is non-empty )
thus ( the charact of P is homogeneous & the charact of P is quasi_total ) ; :: according to UNIALG_1:def 1,UNIALG_1:def 2 :: thesis: P is non-empty
thus the charact of P <> {} ; :: according to UNIALG_1:def 3 :: thesis: the charact of P is non-empty
thus the charact of P is non-empty ; :: thesis: verum