let S be non empty non void bool-correct 4,1 integer BoolSignature ; :: thesis: for X being non-empty ManySortedSet of the carrier of S
for T being b₁,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S
for C being bool-correct 4,1 integer image of T
for I being integer SortSymbol of S
for u being ManySortedFunction of FreeGen T, the Sorts of C holds (\2 (T,I)) value_at (C,u) = 2
let X be non-empty ManySortedSet of the carrier of S; :: thesis: for T being X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S
for C being bool-correct 4,1 integer image of T
for I being integer SortSymbol of S
for u being ManySortedFunction of FreeGen T, the Sorts of C holds (\2 (T,I)) value_at (C,u) = 2
let T be X,S -terms all_vars_including inheriting_operations free_in_itself vf-free integer VarMSAlgebra over S; :: thesis: for C being bool-correct 4,1 integer image of T
for I being integer SortSymbol of S
for u being ManySortedFunction of FreeGen T, the Sorts of C holds (\2 (T,I)) value_at (C,u) = 2
let C be bool-correct 4,1 integer image of T; :: thesis: for I being integer SortSymbol of S
for u being ManySortedFunction of FreeGen T, the Sorts of C holds (\2 (T,I)) value_at (C,u) = 2
let I be integer SortSymbol of S; :: thesis: for u being ManySortedFunction of FreeGen T, the Sorts of C holds (\2 (T,I)) value_at (C,u) = 2
let u be ManySortedFunction of FreeGen T, the Sorts of C; :: thesis: (\2 (T,I)) value_at (C,u) = 2
A1: (\1 (T,I)) value_at (C,u) = 1 by Th52;
thus (\2 (T,I)) value_at (C,u) = ((\1 (T,I)) value_at (C,u)) + ((\1 (T,I)) value_at (C,u)) by Th54
.= 2 by A1, AOFA_A00:55 ; :: thesis: verum