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

proof

let I, J be Instruction of Trivial-COM; :: according to COMPOS_1:def 12 :: 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 is regular :: thesis: Trivial-COM is J/A-independent

proof

let I be Instruction of Trivial-COM; :: according to COMPOS_1:def 14 :: 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; :: according to COMPOS_1:def 15 :: 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 holds
[T,f2,p] in the Instructions of Trivial-COM
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 holds
[T,f2,p] in the Instructions of Trivial-COM
let p be set ; :: thesis: ( f1 in JumpParts T & f2 in product (product" (JumpParts T)) & [T,f1,p] in the Instructions of Trivial-COM implies [T,f2,p] in the Instructions of Trivial-COM )
assume f1 in JumpParts T ; :: thesis: ( not f2 in product (product" (JumpParts T)) or not [T,f1,p] in the Instructions of Trivial-COM or [T,f2,p] in the Instructions of Trivial-COM )
then A1: f1 in {0} by Th86;
assume A2: f2 in product (product" (JumpParts T)) ; :: thesis: ( not [T,f1,p] in the Instructions of Trivial-COM or [T,f2,p] in the Instructions of Trivial-COM )
product" (JumpParts T) = {} by Th86, CARD_3:106;
then ( f1 = 0 & f2 = 0 ) by A1, A2, CARD_3:10, TARSKI:def 1;
hence ( not [T,f1,p] in the Instructions of Trivial-COM or [T,f2,p] in the Instructions of Trivial-COM ) ; :: thesis: verum