let I be non empty set ; :: thesis: for S being non empty non void ManySortedSign
for i being Element of I
for A being MSAlgebra-Family of I,S holds proj A,i is_homomorphism product A,A . i
let S be non empty non void ManySortedSign ; :: thesis: for i being Element of I
for A being MSAlgebra-Family of I,S holds proj A,i is_homomorphism product A,A . i
let i be Element of I; :: thesis: for A being MSAlgebra-Family of I,S holds proj A,i is_homomorphism product A,A . i
let A be MSAlgebra-Family of I,S; :: thesis: proj A,i is_homomorphism product A,A . i
thus proj A,i is_homomorphism product A,A . i :: thesis: verum

proof

let o be OperSymbol of S; :: according to MSUALG_3:def 9 :: thesis: ( Args o,(product A) = {} or for b₁ being Element of Args o,(product A) holds ((proj A,i) . (the_result_sort_of o)) . ((Den o,(product A)) . b₁) = (Den o,(A . i)) . ((proj A,i) # b₁) )
assume Args o,(product A) <> {} ; :: thesis: for b₁ being Element of Args o,(product A) holds ((proj A,i) . (the_result_sort_of o)) . ((Den o,(product A)) . b₁) = (Den o,(A . i)) . ((proj A,i) # b₁)
let x be Element of Args o,(product A); :: thesis: ((proj A,i) . (the_result_sort_of o)) . ((Den o,(product A)) . x) = (Den o,(A . i)) . ((proj A,i) # x)
set F = proj A,i;
set s = the_result_sort_of o;
o in the carrier' of S ;
then A1: o in dom the ResultSort of S by FUNCT_2:def 1;
A2: Result o,(product A) = (the Sorts of (product A) * the ResultSort of S) . o by MSUALG_1:def 10
.= the Sorts of (product A) . (the ResultSort of S . o) by A1, FUNCT_1:23
.= (SORTS A) . (the_result_sort_of o) by MSUALG_1:def 7
.= product (Carrier A,(the_result_sort_of o)) by PRALG_2:def 17 ;
thus ((proj A,i) . (the_result_sort_of o)) . ((Den o,(product A)) . x) = (Den o,(A . i)) . ((proj A,i) # x) :: thesis: verum

proof

per cases ( the_arity_of o = {} or the_arity_of o <> {} ) ;

suppose A3: the_arity_of o = {} ; :: thesis: ((proj A,i) . (the_result_sort_of o)) . ((Den o,(product A)) . x) = (Den o,(A . i)) . ((proj A,i) # x)

then const o,(product A) in product (Carrier A,(the_result_sort_of o)) by A2, Th6;
then A4: const o,(product A) in dom (proj (Carrier A,(the_result_sort_of o)),i) by CARD_3:def 17;
A5: Args o,(product A) = {{} } by A3, PRALG_2:11;
then A6: x = {} by TARSKI:def 1;
((proj A,i) . (the_result_sort_of o)) . ((Den o,(product A)) . x) = ((proj A,i) . (the_result_sort_of o)) . (const o,(product A)) by A5, TARSKI:def 1
.= (proj (Carrier A,(the_result_sort_of o)),i) . (const o,(product A)) by Def3
.= (const o,(product A)) . i by A4, CARD_3:def 17
.= const o,(A . i) by A3, Th10
.= (Den o,(A . i)) . ((proj A,i) # x) by A3, A6, Th12 ;
hence ((proj A,i) . (the_result_sort_of o)) . ((Den o,(product A)) . x) = (Den o,(A . i)) . ((proj A,i) # x) ; :: thesis: verum

end;

suppose A7: the_arity_of o <> {} ; :: thesis: ((proj A,i) . (the_result_sort_of o)) . ((Den o,(product A)) . x) = (Den o,(A . i)) . ((proj A,i) # x)

reconsider D = (Den o,(product A)) . x as Function by A2;
(Den o,(product A)) . x in product (Carrier A,(the_result_sort_of o)) by A2;
then A8: (Den o,(product A)) . x in dom (proj (Carrier A,(the_result_sort_of o)),i) by CARD_3:def 17;
((proj A,i) . (the_result_sort_of o)) . ((Den o,(product A)) . x) = (proj (Carrier A,(the_result_sort_of o)),i) . ((Den o,(product A)) . x) by Def3
.= D . i by A8, CARD_3:def 17
.= (Den o,(A . i)) . ((commute x) . i) by A7, Th23
.= (Den o,(A . i)) . ((proj A,i) # x) by A7, Th24 ;
hence ((proj A,i) . (the_result_sort_of o)) . ((Den o,(product A)) . x) = (Den o,(A . i)) . ((proj A,i) # x) ; :: thesis: verum

end;

end;

end;

end;