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 7 :: 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 5
.= the Sorts of (product A) . ( the ResultSort of S . o) by A1, FUNCT_1:13
.= (SORTS A) . (the_result_sort_of o) by MSUALG_1:def 2
.= product (Carrier (A,(the_result_sort_of o))) by PRALG_2:def 10 ;
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, Th5;
then A4: const (o,(product A)) in dom (proj ((Carrier (A,(the_result_sort_of o))),i)) by CARD_3:def 16;
A5: Args (o,(product A)) = {{}} by A3, PRALG_2:4;
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 Def2
.= (const (o,(product A))) . i by A4, CARD_3:def 16
.= const (o,(A . i)) by A3, Th9
.= (Den (o,(A . i))) . ((proj (A,i)) # x) by A3, A6, Th11 ;
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 16;
((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 Def2
.= D . i by A8, CARD_3:def 16
.= (Den (o,(A . i))) . ((commute x) . i) by A7, Th22
.= (Den (o,(A . i))) . ((proj (A,i)) # x) by A7, Th23 ;
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;