thus Trivial-COM N is homogeneous :: thesis: ( Trivial-COM N is regular & Trivial-COM N is J/A-independent )

proof

let I, J be Instruction of (Trivial-COM N); :: according to COMPOS_1:def 33 :: thesis: ( InsCode I = InsCode J implies dom (JumpPart I) = dom (JumpPart J) )
( JumpPart I = {} & JumpPart J = {} ) by Th85;
hence ( InsCode I = InsCode J implies dom (JumpPart I) = dom (JumpPart J) ) ; :: thesis: verum

end;

thus Trivial-COM N is regular :: thesis: Trivial-COM N is J/A-independent

proof

let I be Instruction of (Trivial-COM N); :: according to COMPOS_1:def 35 :: thesis: for k being set st k in dom (JumpPart I) holds
(product" (JumpParts (InsCode I))) . k = NAT
JumpPart I = {} by Th85;
hence for k being set st k in dom (JumpPart I) holds
(product" (JumpParts (InsCode I))) . k = NAT ; :: thesis: verum

end;

let T be InsType of (Trivial-COM N); :: according to COMPOS_1:def 36 :: thesis: for f1, f2 being Function
for p being set st f1 in JumpParts T & f2 in product (product" (JumpParts T)) & [T,f1,p] in the Instructions of (Trivial-COM N) holds
[T,f2,p] in the Instructions of (Trivial-COM N)
let f1, f2 be Function; :: thesis: for p being set st f1 in JumpParts T & f2 in product (product" (JumpParts T)) & [T,f1,p] in the Instructions of (Trivial-COM N) holds
[T,f2,p] in the Instructions of (Trivial-COM N)
let p be set ; :: thesis: ( f1 in JumpParts T & f2 in product (product" (JumpParts T)) & [T,f1,p] in the Instructions of (Trivial-COM N) implies [T,f2,p] in the Instructions of (Trivial-COM N) )
assume f1 in JumpParts T ; :: thesis: ( not f2 in product (product" (JumpParts T)) or not [T,f1,p] in the Instructions of (Trivial-COM N) or [T,f2,p] in the Instructions of (Trivial-COM N) )
then A: f1 in {0} by Th86;
assume Z: f2 in product (product" (JumpParts T)) ; :: thesis: ( not [T,f1,p] in the Instructions of (Trivial-COM N) or [T,f2,p] in the Instructions of (Trivial-COM N) )
product" (JumpParts T) = {} by Th86, CARD_3:156;
then ( f1 = 0 & f2 = 0 ) by A, Z, CARD_3:19, TARSKI:def 1;
hence ( not [T,f1,p] in the Instructions of (Trivial-COM N) or [T,f2,p] in the Instructions of (Trivial-COM N) ) ; :: thesis: verum